rng (X --> x) c= NAT by MEMBERED:6;
hence X --> x is natural-valued by Def6; :: thesis: verum