let GX be non empty TopSpace; :: thesis: for A, B, C being Subset of GX st C is a_component & A c= C & B is connected & Cl A meets Cl B holds

B c= C

let A, B, C be Subset of GX; :: thesis: ( C is a_component & A c= C & B is connected & Cl A meets Cl B implies B c= C )

assume that

A1: C is a_component and

A2: A c= C and

A3: B is connected and

A4: (Cl A) /\ (Cl B) <> {} ; :: according to XBOOLE_0:def 7 :: thesis: B c= C

consider p being Point of GX such that

A5: p in (Cl A) /\ (Cl B) by A4, SUBSET_1:4;

reconsider C9 = C as Subset of GX ;

C9 is closed by A1, CONNSP_1:33;

then Cl C = C by PRE_TOPC:22;

then A6: Cl A c= C by A2, PRE_TOPC:19;

p in Cl A by A5, XBOOLE_0:def 4;

then A7: Component_of p = C9 by A1, A6, CONNSP_1:41;

p in Cl B by A5, XBOOLE_0:def 4;

then A8: Cl B c= Component_of p by A3, Th1, CONNSP_1:19;

B c= Cl B by PRE_TOPC:18;

hence B c= C by A7, A8; :: thesis: verum

B c= C

let A, B, C be Subset of GX; :: thesis: ( C is a_component & A c= C & B is connected & Cl A meets Cl B implies B c= C )

assume that

A1: C is a_component and

A2: A c= C and

A3: B is connected and

A4: (Cl A) /\ (Cl B) <> {} ; :: according to XBOOLE_0:def 7 :: thesis: B c= C

consider p being Point of GX such that

A5: p in (Cl A) /\ (Cl B) by A4, SUBSET_1:4;

reconsider C9 = C as Subset of GX ;

C9 is closed by A1, CONNSP_1:33;

then Cl C = C by PRE_TOPC:22;

then A6: Cl A c= C by A2, PRE_TOPC:19;

p in Cl A by A5, XBOOLE_0:def 4;

then A7: Component_of p = C9 by A1, A6, CONNSP_1:41;

p in Cl B by A5, XBOOLE_0:def 4;

then A8: Cl B c= Component_of p by A3, Th1, CONNSP_1:19;

B c= Cl B by PRE_TOPC:18;

hence B c= C by A7, A8; :: thesis: verum