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 ) )
A1: ( A c= A \/ B & B c= A \/ B ) by XBOOLE_1:7;
A2: 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 that
A3: C is connected and
A4: D is connected and
A5: C /\ D <> {} ; :: thesis: C \/ D c= Component_of C
C meets D by A5;
then A6: C \/ D is connected by A3, A4, CONNSP_1:1, CONNSP_1:17;
C <> {} by A5;
hence C \/ D c= Component_of C by A3, A6, Th14; :: thesis: verum
end;
assume ( 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 )
then ( A \/ B c= Component_of A & A \/ B c= Component_of B ) by A2;
hence ( A \/ B c= Component_of A & A \/ B c= Component_of B & A c= Component_of B & B c= Component_of A ) by A1; :: thesis: verum