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