let R be Relation of X,Y; :: thesis: R is real-valued
thus rng R c= REAL by MEMBERED:3; :: according to VALUED_0:def 3 :: thesis: verum