rng [:X,Y:] c= Y by RELAT_1:194;
hence rng [:X,Y:] c= INT by MEMBERED:5; :: according to VALUED_0:def 5 :: thesis: verum