let X, Y, Z, x be set ; :: thesis: ( X misses Y & x in X /\ Z implies not x in Y /\ Z )
assume that
A1: X misses Y and
A2: x in X /\ Z ; :: thesis: not x in Y /\ Z
X /\ Z misses Y /\ Z by A1, XBOOLE_1:76;
hence not x in Y /\ Z by A2, XBOOLE_0:3; :: thesis: verum