thus ( dom (id X) c= X & rng (id X) c= X ) by Th71; :: according to RELAT_1:def 18,RELAT_1:def 19 :: thesis: verum