let f be Relation; :: thesis: ( f is NAT -valued iff rng f is natural-membered )
( f is NAT -valued iff f is natural-valued ) ;
hence ( f is NAT -valued iff rng f is natural-membered ) by NV; :: thesis: verum