rng [:X,Y:] c= Y by RELAT_1:159;
hence rng [:X,Y:] c= RAT by MEMBERED:4; :: according to RELAT_1:def 19 :: thesis: verum