let G be TopSpace; :: thesis: for A, B, C being Subset of G st A is a_component & B is a_component & C is connected & A meets C & B meets C holds
A = B
let A, B, C be Subset of G; :: thesis: ( A is a_component & B is a_component & C is connected & A meets C & B meets C implies A = B )
assume that
A1: A is a_component and
A2: B is a_component and
A3: C is connected and
A4: A meets C and
A5: B meets C ; :: thesis: A = B
A6: ( C /\ A = {} G or C c= A ) by A1, A3, A4, CONNSP_1:36;
A7: ( C misses B or C c= B ) by A2, A3, CONNSP_1:36;

per cases ( A = B or A misses B ) by A1, A2, CONNSP_1:1, CONNSP_1:34;

suppose A = B ; :: thesis: A = B

hence A = B ; :: thesis: verum

end;

suppose A misses B ; :: thesis: A = B

then A8: A /\ B = {} ;
C c= A /\ B by A4, A5, A6, A7, XBOOLE_1:19;
then C = {} by A8;
then C /\ A = {} ;
hence A = B by A4; :: thesis: verum

end;

end;