theorem :: ZFMISC_1:28

for x, x1, y, y1 being object holds
( [x,y] in [:{x1},{y1}:] iff ( x = x1 & y = y1 ) )