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

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

( 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

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 )
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 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

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