rng R c= ExtREAL by Def2;
hence rng R is ext-real-membered ; :: thesis: verum