let GX be non empty TopSpace; :: thesis: for A, B, C being Subset of GX st C is_a_component_of GX & 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_of GX & A c= C & B is connected & Cl A meets Cl B implies B c= C )
assume A1: ( C is_a_component_of GX & A c= C & B is connected & (Cl A) /\ (Cl B) <> {} ) ; :: according to XBOOLE_0:def 7 :: thesis: B c= C
then consider p being Point of GX such that
A2: p in (Cl A) /\ (Cl B) by SUBSET_1:10;
reconsider C' = C as Subset of GX ;
C' is closed by A1, CONNSP_1:35;
then Cl C = C by PRE_TOPC:52;
then A3: Cl A c= C by A1, PRE_TOPC:49;
A4: ( p in Cl A & p in Cl B ) by A2, XBOOLE_0:def 4;
then A5: Component_of p = C' by A1, A3, CONNSP_1:44;
A6: Cl B c= Component_of p by A1, A4, Th1, CONNSP_1:20;
B c= Cl B by PRE_TOPC:48;
hence B c= C by A5, A6, XBOOLE_1:1; :: thesis: verum