let X, Y, Z be set ; :: thesis: ( X misses Y \ Z implies Y misses X \ Z )
X /\ (Y \ Z) = (Y /\ X) \ Z by Th49
.= Y /\ (X \ Z) by Th49 ;
hence ( X misses Y \ Z implies Y misses X \ Z ) ; :: thesis: verum