theorem :: ZFMISC_1:5

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