rng R c= NAT by Def6;
hence rng R is natural-membered ; :: thesis: verum