A1: Y c= ExtREAL by MEMBERED:2;
rng [:X,Y:] c= Y by RELAT_1:194;
hence rng [:X,Y:] c= ExtREAL by A1, XBOOLE_1:1; :: according to VALUED_0:def 2 :: thesis: verum