let X, Y be set ; :: thesis: X \ Y misses Y
for x being object holds not x in (X \ Y) /\ Y

proof

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;

hence (X \ Y) /\ Y = {} by XBOOLE_0:def 1; :: according to XBOOLE_0:def 7 :: thesis: verum