let X, Y be set ; :: thesis: X \ (X /\ Y) misses Y
X \ (X /\ Y) = X \ Y by Th47;
hence X \ (X /\ Y) misses Y by Th79; :: thesis: verum