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