let R be Relation; :: thesis: ( R is rational-valued implies R is real-valued )
assume rng R c= RAT ; :: according to VALUED_0:def 4 :: thesis: R is real-valued
hence rng R c= REAL by NUMBERS:12, XBOOLE_1:1; :: according to VALUED_0:def 3 :: thesis: verum