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