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