( rng R c= ExtREAL & rng (R | X) c= rng R ) by Def2, RELAT_1:99;
hence rng (R | X) c= ExtREAL by XBOOLE_1:1; :: according to VALUED_0:def 2 :: thesis: verum