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 )

hence
X /\ Y misses X \ Y
by XBOOLE_0:3; :: thesis: verum( 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;( 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