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

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