theorem :: GLIBPRE0:5

for a, b, x, y being object holds
( {a,b} = {x,y} iff ( ( x = a & y = b ) or ( x = b & y = a ) ) ) by ZFMISC_1:22;