rng [:X,Y:] c= Y by RELAT_1:159;
hence rng [:X,Y:] c= REAL by MEMBERED:3; :: according to VALUED_0:def 3 :: thesis: verum