let X, Y, Z be set ; :: thesis: ( Y misses Z implies X /\ Y misses X /\ Z )
assume Y misses Z ; :: thesis: X /\ Y misses X /\ Z
then X /\ Z misses Y by Th74;
hence X /\ Y misses X /\ Z by Th74; :: thesis: verum