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