rng R c= INT by Def5;
hence rng R is integer-membered ; :: thesis: verum