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 S1[ object ] means ( $1 in X iff $1 in Y );
thus ( X = Y implies for x being set st x in X \/ Y holds
S1[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
S1[x] ; :: thesis: X = Y
now :: thesis: for x being object holds S1[x]
let x be object ; :: thesis: S1[b1]
per cases ( x in X \/ Y or not x in X \/ Y ) ;
end;
end;
hence X = Y by TARSKI:2; :: thesis: verum