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)

x in X \ (X \ Y) :: according to TARSKI:def 3 :: thesis: verum

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

thus
for x being object st x in X /\ Y holds
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;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

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;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