let A, B, C, D be set ; :: thesis: ( B misses D & A c= B & C c= D implies A misses C )
assume A1: ( B misses D & A c= B & C c= D ) ; :: thesis: A misses C
assume A meets C ; :: thesis: contradiction
then consider x being set such that
A2: x in A /\ C by XBOOLE_0:4;
A /\ C c= B /\ D by A1, XBOOLE_1:27;
hence contradiction by A1, A2, XBOOLE_0:4; :: thesis: verum