let X, Y be set ; :: thesis: X \ (X /\ Y) = X \ Y

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

let x be object ; :: thesis: ( x in X \ (X /\ Y) iff x in X \ Y )
( x in X & not x in X /\ Y iff ( x in X & not x in Y ) ) by XBOOLE_0:def 4;
hence ( x in X \ (X /\ Y) iff x in X \ Y ) by XBOOLE_0:def 5; :: thesis: verum

end;

hence X \ (X /\ Y) = X \ Y by TARSKI:2; :: thesis: verum