thus rng (id X) c= INT by MEMBERED:5; :: according to RELAT_1:def 19 :: thesis: verum