let GX be non empty TopSpace; :: thesis: for A, B being non empty Subset of GX st A c= B & A is connected holds
ex C being Subset of GX st
( C is_a_component_of B & A c= C )
let A, B be non empty Subset of GX; :: thesis: ( A c= B & A is connected implies ex C being Subset of GX st
( C is_a_component_of B & A c= C ) )
assume that
A1: A c= B and
A2: A is connected ; :: thesis: ex C being Subset of GX st
( C is_a_component_of B & A c= C )
consider p being object such that
A3: p in A by XBOOLE_0:def 1;
A4: B = [#] (GX | B) by PRE_TOPC:def 5
.= the carrier of (GX | B) ;
then reconsider p = p as Point of (GX | B) by A1, A3;
reconsider C = Component_of p as Subset of GX by PRE_TOPC:11;
take C ; :: thesis: ( C is_a_component_of B & A c= C )
A5: Component_of p is a_component by CONNSP_1:40;
hence C is_a_component_of B by CONNSP_1:def 6; :: thesis: A c= C
reconsider AA = A as Subset of (GX | B) by A1, A4;
GX | A is connected by A2, CONNSP_1:def 3;
then (GX | B) | AA is connected by Th2;
then A6: AA is connected by CONNSP_1:def 3;
p in Component_of p by CONNSP_1:38;
then AA /\ (Component_of p) <> {} (GX | B) by A3, XBOOLE_0:def 4;
then AA meets Component_of p ;
hence A c= C by A5, A6, CONNSP_1:36; :: thesis: verum