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

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