theorem Th3: :: ZFMISC_1:3

for x, y being object st {x} c= {y} holds
x = y