let X, Y be set ; :: thesis: X /\ Y misses X \+\ Y
( X /\ Y misses X \ Y & X /\ Y misses Y \ X ) by Th89;
hence X /\ Y misses X \+\ Y by Th70; :: thesis: verum