let X, Y, Z be set ; :: thesis: ( X meets Y & X misses Z implies X meets Y \ Z )
assume that
A1: X meets Y and
A2: X misses Z ; :: thesis: X meets Y \ Z
X /\ (Y \ Z) = (X /\ Y) \ (X /\ Z) by Th50
.= (X /\ Y) \ {} by A2 ;
hence X /\ (Y \ Z) <> {} by A1; :: according to XBOOLE_0:def 7 :: thesis: verum