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

assume A1: X \ Y = Y \ X ; :: thesis: 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 )

hence
X = Y
by TARSKI:2; :: thesis: verum( 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;( ( 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