thus rng (id X) c= ExtREAL by MEMBERED:2; :: according to VALUED_0:def 2 :: thesis: verum