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 )

hence
X \ (X /\ Y) = X \ Y
by TARSKI:2; :: thesis: verum( 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;( 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