X c= REAL by MEMBERED:3;
hence rng (id X) c= REAL by RELAT_1:71; :: according to VALUED_0:def 3 :: thesis: verum