let G be non empty TopSpace; :: thesis: for A, B, C, D being Subset of G st B is a_component & C is a_component & 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 & C is a_component & A \/ B = the carrier of G & C misses A implies C = B )
assume that
A1: B is a_component and
A2: C is a_component and
A3: A \/ B = the carrier of G and
A4: C misses A ; :: thesis: C = B

now :: thesis: not C misses B

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 = {} ;
C <> {} G by A2, CONNSP_1:32;
hence contradiction by A4, A6, A5; :: thesis: verum

end;

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