let R be Relation; :: thesis: ( R is natural-valued implies R is NAT -valued )
assume R is natural-valued ; :: thesis: R is NAT -valued
then rng R c= NAT by VALUED_0:def 6;
hence R is NAT -valued by RELAT_1:def 19; :: thesis: verum