theorem :: ZFMISC_1:18

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