A1: rng R c= REAL by Def3;
rng (R | X) c= rng R by RELAT_1:99;
hence rng (R | X) c= REAL by A1, XBOOLE_1:1; :: according to VALUED_0:def 3 :: thesis: verum