let X, Y, Z be set ; :: thesis: ( ( for x being object holds
( not x in X iff ( x in Y iff x in Z ) ) ) implies X = Y \+\ Z )
assume A1: for x being object holds
( not x in X iff ( x in Y iff x in Z ) ) ; :: thesis: X = Y \+\ Z

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

let x be object ; :: thesis: ( x in X iff x in Y \+\ Z )
( x in X iff ( ( x in Y & not x in Z ) or ( x in Z & not x in Y ) ) ) by A1;
then ( x in X iff ( x in Y \ Z or x in Z \ Y ) ) by Def5;
hence ( x in X iff x in Y \+\ Z ) by Def3; :: thesis: verum

end;

hence X = Y \+\ Z by TARSKI:2; :: thesis: verum