let G be non empty TopSpace; :: thesis: for A, B, C, D being Subset of G st A is_a_component_of G & 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: ( A is_a_component_of G & 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 A1: ( A is_a_component_of G & B is_a_component_of G & C is_a_component_of G & A \/ B = the carrier of G & C misses A ) ; :: thesis: C = B

now

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

end;

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