let A, B, X be set ; :: thesis: ( X c= A \+\ B iff ( X c= A \/ B & X misses A /\ B ) )
A \+\ B = (A \/ B) \ (A /\ B) by Lm5;
hence ( X c= A \+\ B iff ( X c= A \/ B & X misses A /\ B ) ) by Th86, Th106; :: thesis: verum