let R be Relation; :: thesis: ( R is INT -valued implies R is integer-valued )
assume R is INT -valued ; :: thesis: R is integer-valued
hence rng R c= INT by RELAT_1:def 19; :: according to VALUED_0:def 5 :: thesis: verum