let R be Relation; :: thesis: ( R is integer-valued implies R is rational-valued )
assume rng R c= INT ; :: according to VALUED_0:def 5 :: thesis: R is rational-valued
hence rng R c= RAT by NUMBERS:14, XBOOLE_1:1; :: according to VALUED_0:def 4 :: thesis: verum