let GX be non empty TopSpace; :: thesis: for A, B being Subset of GX st A is connected & B is connected & A meets B holds
( A \/ B c= Component_of A & A \/ B c= Component_of B & A c= Component_of B & B c= Component_of A )
let A, B be Subset of GX; :: thesis: ( A is connected & B is connected & A meets B implies ( A \/ B c= Component_of A & A \/ B c= Component_of B & A c= Component_of B & B c= Component_of A ) )
assume A1: ( A is connected & B is connected & A /\ B <> {} ) ; :: according to XBOOLE_0:def 7 :: thesis: ( A \/ B c= Component_of A & A \/ B c= Component_of B & A c= Component_of B & B c= Component_of A )
for C, D being Subset of GX st C is connected & D is connected & C /\ D <> {} holds
C \/ D c= Component_of C

proof

let C, D be Subset of GX; :: thesis: ( C is connected & D is connected & C /\ D <> {} implies C \/ D c= Component_of C )
assume A2: ( C is connected & D is connected & C /\ D <> {} ) ; :: thesis: C \/ D c= Component_of C
then A3: C <> {} ;
C meets D by A2, XBOOLE_0:def 7;
then C \/ D is connected by A2, CONNSP_1:2, CONNSP_1:18;
hence C \/ D c= Component_of C by A2, A3, Th14; :: thesis: verum

end;

then A4: ( A \/ B c= Component_of A & A \/ B c= Component_of B ) by A1;
( A c= A \/ B & B c= A \/ B ) by XBOOLE_1:7;
hence ( A \/ B c= Component_of A & A \/ B c= Component_of B & A c= Component_of B & B c= Component_of A ) by A4, XBOOLE_1:1; :: thesis: verum