let X, Y be set ; 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 ; ( 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; verum