let X, Y be set ; :: thesis: ( X \ Y = Y \ X implies X = Y )
assume A1: X \ Y = Y \ X ; :: thesis: X = Y

now :: thesis: for x being object holds
( x in X iff x in Y )

let x be object ; :: thesis: ( x in X iff x in Y )
( ( x in X & not x in Y ) iff x in Y \ X ) by A1, XBOOLE_0:def 5;
hence ( x in X iff x in Y ) by XBOOLE_0:def 5; :: thesis: verum

end;

hence X = Y by TARSKI:2; :: thesis: verum