let R be Relation; :: thesis: for S being rational-valued Relation st R c= S holds
R is rational-valued
let S be rational-valued Relation; :: thesis: ( R c= S implies R is rational-valued )
assume R c= S ; :: thesis: R is rational-valued
then A1: rng R c= rng S by RELAT_1:11;
rng S c= RAT by Def3r;
hence rng R c= RAT by A1; :: according to VALUED_0:def 4 :: thesis: verum