let a, b, x, y be object ; :: thesis: ( a <> b & x = the Element of {a,b} & y = the Element of {a,b} \ { the Element of {a,b}} & not ( x = a & y = b ) implies ( x = b & y = a ) )
assume A1: ( a <> b & x = the Element of {a,b} & y = the Element of {a,b} \ { the Element of {a,b}} ) ; :: thesis: ( ( x = a & y = b ) or ( x = b & y = a ) )

per cases then ( x = a or x = b ) by TARSKI:def 2;

suppose A2: x = a ; :: thesis: ( ( x = a & y = b ) or ( x = b & y = a ) )

{a,b} \ {a} = {b} by A1, ZFMISC_1:17;
hence ( ( x = a & y = b ) or ( x = b & y = a ) ) by A1, A2, TARSKI:def 1; :: thesis: verum

end;

suppose A3: x = b ; :: thesis: ( ( x = a & y = b ) or ( x = b & y = a ) )

{a,b} \ {b} = {a} by A1, ZFMISC_1:17;
hence ( ( x = a & y = b ) or ( x = b & y = a ) ) by A1, A3, TARSKI:def 1; :: thesis: verum

end;

end;