let X, Y be set ; :: thesis: X \ (X \ Y) = X /\ Y
thus for x being set st x in X \ (X \ Y) holds
x in X /\ Y :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: X /\ Y c= X \ (X \ Y)

proof

let x be set ; :: thesis: ( x in X \ (X \ Y) implies x in X /\ Y )
assume x in X \ (X \ Y) ; :: thesis: x in X /\ Y
then ( x in X & not x in X \ Y ) by XBOOLE_0:def 5;
then ( x in X & ( not x in X or x in Y ) ) by XBOOLE_0:def 5;
hence x in X /\ Y by XBOOLE_0:def 4; :: thesis: verum

end;

thus for x being set st x in X /\ Y holds
x in X \ (X \ Y) :: according to TARSKI:def 3 :: thesis: verum

proof

let x be set ; :: thesis: ( x in X /\ Y implies x in X \ (X \ Y) )
assume x in X /\ Y ; :: thesis: x in X \ (X \ Y)
then ( x in X & ( not x in X or x in Y ) ) by XBOOLE_0:def 4;
then ( x in X & not x in X \ Y ) by XBOOLE_0:def 5;
hence x in X \ (X \ Y) by XBOOLE_0:def 5; :: thesis: verum

end;