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

now :: thesis: for x being object holds
( not x in X /\ Y or not x in X \ Y )

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

end;

hence X /\ Y misses X \ Y by XBOOLE_0:3; :: thesis: verum