let X, Y be set ; :: thesis: X \ (X \ Y) = X /\ Y
thus for x being object 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 object ; :: thesis: ( x in X \ (X \ Y) implies x in X /\ Y )
assume A1: x in X \ (X \ Y) ; :: thesis: x in X /\ Y
then not x in X \ Y by XBOOLE_0:def 5;
then A2: ( not x in X or x in Y ) by XBOOLE_0:def 5;
x in X by A1, XBOOLE_0:def 5;
hence x in X /\ Y by A2, XBOOLE_0:def 4; :: thesis: verum

end;

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

proof

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

end;