let G be non empty TopSpace; :: thesis: for A, B, C, D being Subset of G st B is_a_component_of G & C is_a_component_of G & A \/ B = the carrier of G & C misses A holds
C = B
let A, B, C, D be Subset of G; :: thesis: ( B is_a_component_of G & C is_a_component_of G & A \/ B = the carrier of G & C misses A implies C = B )
assume that
A1: B is_a_component_of G and
A2: C is_a_component_of G and
A3: A \/ B = the carrier of G and
A4: C misses A ; :: thesis: C = B

now

C /\ the carrier of G = C by XBOOLE_1:28;
then A5: (C /\ A) \/ (C /\ B) = C by A3, XBOOLE_1:23;
assume C misses B ; :: thesis: contradiction
then A6: C /\ B = {} by XBOOLE_0:def 7;
C <> {} G by A2, CONNSP_1:34;
hence contradiction by A4, A6, A5, XBOOLE_0:def 7; :: thesis: verum

end;

hence C = B by A1, A2, CONNSP_1:37; :: thesis: verum