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