let X, Y be set ; :: thesis: ( X = Y iff for x being set st x in X \/ Y holds
( x in X iff x in Y ) )
set Z = X \/ Y;
defpred S₁[ object ] means ( $1 in X iff $1 in Y );
thus ( X = Y implies for x being set st x in X \/ Y holds
S₁[x] ) ; :: thesis: ( ( for x being set st x in X \/ Y holds
( x in X iff x in Y ) ) implies X = Y )
assume A1: for x being set st x in X \/ Y holds
S₁[x] ; :: thesis: X = Y

now :: thesis: for x being object holds S₁[x]

let x be object ; :: thesis: S₁[b₁]

per cases ( x in X \/ Y or not x in X \/ Y ) ;

suppose x in X \/ Y ; :: thesis: S₁[b₁]

hence S₁[x] by A1; :: thesis: verum

end;

suppose not x in X \/ Y ; :: thesis: S₁[b₁]

hence S₁[x] by XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

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