let X, Y be set ; :: thesis: for x being object holds
( x in X \+\ Y iff ( ( x in X & not x in Y ) or ( x in Y & not x in X ) ) )
let x be object ; :: thesis: ( x in X \+\ Y iff ( ( x in X & not x in Y ) or ( x in Y & not x in X ) ) )
( x in X \+\ Y iff ( x in X \ Y or x in Y \ X ) ) by Def3;
hence ( x in X \+\ Y iff ( ( x in X & not x in Y ) or ( x in Y & not x in X ) ) ) by Def5; :: thesis: verum