let X, Y, Z be set ; :: thesis: ( X misses Y \ Z implies Y misses X \ Z )
A1: ( X misses Y \ Z iff X /\ (Y \ Z) = {} ) by XBOOLE_0:def 7;
X /\ (Y \ Z) = (Y /\ X) \ Z by Th49
.= Y /\ (X \ Z) by Th49 ;
hence ( X misses Y \ Z implies Y misses X \ Z ) by A1, XBOOLE_0:def 7; :: thesis: verum