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

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