let R be Relation; :: thesis: ( R is natural-valued implies R is integer-valued )
assume rng R c= NAT ; :: according to VALUED_0:def 6 :: thesis: R is integer-valued
hence rng R c= INT by NUMBERS:17; :: according to VALUED_0:def 5 :: thesis: verum