let A be set ; :: thesis: for B, C, D being Subset of A st B \ C = {} holds
B misses D \ C
let B, C, D be Subset of A; :: thesis: ( B \ C = {} implies B misses D \ C )
assume B \ C = {} ; :: thesis: B misses D \ C
then A1: B c= C by XBOOLE_1:37;
C misses D \ C by XBOOLE_1:79;
hence B misses D \ C by A1, XBOOLE_1:63; :: thesis: verum