theorem Th4: :: ZFMISC_1:4

for x, y1, y2 being object st {x} = {y1,y2} holds
x = y1