theorem Th4: :: ABCMIZ_1:4

for X, Y being set holds (id X) .: Y c= Y