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