rng R c= REAL by Def3;
hence rng R is real-membered ; :: thesis: verum