let X, Y, Z be set ; :: thesis: ( X misses Y implies X misses Y \ Z )
assume A1: X misses Y ; :: thesis: X misses Y \ Z
assume X meets Y \ Z ; :: thesis: contradiction
then consider x being object such that
A2: x in X and
A3: x in Y \ Z by XBOOLE_0:3;
x in Y by A3, XBOOLE_0:def 5;
hence contradiction by A1, A2, XBOOLE_0:3; :: thesis: verum