let X, Y, Z be set ; :: thesis: X /\ Z misses Y \ Z
(X /\ Z) /\ (Y \ Z) = X /\ (Z /\ (Y \ Z)) by XBOOLE_1:16
.= X /\ ((Z /\ Y) \ (Z /\ Z)) by XBOOLE_1:50
.= X /\ {} by XBOOLE_1:17, XBOOLE_1:37
.= {} ;
hence X /\ Z misses Y \ Z by XBOOLE_0:def 7; :: thesis: verum