let R be Relation; :: thesis: ( R is empty implies R is natural-valued )
assume R is empty ; :: thesis: R is natural-valued
hence rng R c= NAT by RELAT_1:38, XBOOLE_1:2; :: according to VALUED_0:def 6 :: thesis: verum