( rng R c= RAT & rng (R | X) c= rng R ) by Def3r, RELAT_1:70;
hence rng (R | X) c= RAT ; :: according to VALUED_0:def 4 :: thesis: verum