let X, Y be set ; :: thesis: X \ Y misses Y

for x being object holds not x in (X \ Y) /\ Y

for x being object holds not x in (X \ Y) /\ Y

proof

hence
(X \ Y) /\ Y = {}
by XBOOLE_0:def 1; :: according to XBOOLE_0:def 7 :: thesis: verum
given x being object such that A1:
x in (X \ Y) /\ Y
; :: thesis: contradiction

( x in X \ Y & x in Y ) by A1, XBOOLE_0:def 4;

hence contradiction by XBOOLE_0:def 5; :: thesis: verum

end;( x in X \ Y & x in Y ) by A1, XBOOLE_0:def 4;

hence contradiction by XBOOLE_0:def 5; :: thesis: verum