let X be non empty TopSpace; :: thesis: ( X is locally_connected implies for E being non empty Subset of X

for C being non empty Subset of (X | E) st C is connected & C is open holds

ex H being Subset of X st

( H is open & H is connected & C = E /\ H ) )

assume A1: X is locally_connected ; :: thesis: for E being non empty Subset of X

for C being non empty Subset of (X | E) st C is connected & C is open holds

ex H being Subset of X st

( H is open & H is connected & C = E /\ H )

let E be non empty Subset of X; :: thesis: for C being non empty Subset of (X | E) st C is connected & C is open holds

ex H being Subset of X st

( H is open & H is connected & C = E /\ H )

let C be non empty Subset of (X | E); :: thesis: ( C is connected & C is open implies ex H being Subset of X st

( H is open & H is connected & C = E /\ H ) )

assume that

A2: C is connected and

A3: C is open ; :: thesis: ex H being Subset of X st

( H is open & H is connected & C = E /\ H )

C in the topology of (X | E) by A3, PRE_TOPC:def 2;

then consider G being Subset of X such that

A4: G in the topology of X and

A5: C = G /\ ([#] (X | E)) by PRE_TOPC:def 4;

A6: C = G /\ E by A5, PRE_TOPC:def 5;

reconsider G = G as non empty Subset of X by A5;

A7: G is open by A4, PRE_TOPC:def 2;

reconsider C1 = C as Subset of X by PRE_TOPC:11;

C <> {} (X | E) ;

then consider x being Point of (X | E) such that

A8: x in C by PRE_TOPC:12;

x in G by A5, A8, XBOOLE_0:def 4;

then x in [#] (X | G) by PRE_TOPC:def 5;

then reconsider y = x as Point of (X | G) ;

set H1 = Component_of y;

reconsider H = Component_of y as Subset of X by PRE_TOPC:11;

take H ; :: thesis: ( H is open & H is connected & C = E /\ H )

A9: Component_of y is a_component by CONNSP_1:40;

then H is_a_component_of G by CONNSP_1:def 6;

hence H is open by A1, A7, Th18; :: thesis: ( H is connected & C = E /\ H )

C c= G by A5, XBOOLE_1:17;

then C c= [#] (X | G) by PRE_TOPC:def 5;

then reconsider C2 = C1 as Subset of (X | G) ;

Component_of y c= [#] (X | G) ;

then A10: H c= G by PRE_TOPC:def 5;

C1 is connected by A2, CONNSP_1:23;

then C2 is connected by CONNSP_1:23;

then ( C2 misses H or C2 c= H ) by A9, CONNSP_1:36;

then A11: ( C2 /\ H = {} (X | G) or C2 c= H ) by XBOOLE_0:def 7;

A12: x in Component_of y by CONNSP_1:38;

H /\ (G /\ E) c= C by A6, XBOOLE_0:def 4;

then (H /\ G) /\ E c= C by XBOOLE_1:16;

then A13: E /\ H c= C by A10, XBOOLE_1:28;

thus H is connected by CONNSP_1:23; :: thesis: C = E /\ H

C c= E by A6, XBOOLE_1:17;

then C c= E /\ H by A8, A11, A12, XBOOLE_0:def 4;

hence C = E /\ H by A13, XBOOLE_0:def 10; :: thesis: verum

for C being non empty Subset of (X | E) st C is connected & C is open holds

ex H being Subset of X st

( H is open & H is connected & C = E /\ H ) )

assume A1: X is locally_connected ; :: thesis: for E being non empty Subset of X

for C being non empty Subset of (X | E) st C is connected & C is open holds

ex H being Subset of X st

( H is open & H is connected & C = E /\ H )

let E be non empty Subset of X; :: thesis: for C being non empty Subset of (X | E) st C is connected & C is open holds

ex H being Subset of X st

( H is open & H is connected & C = E /\ H )

let C be non empty Subset of (X | E); :: thesis: ( C is connected & C is open implies ex H being Subset of X st

( H is open & H is connected & C = E /\ H ) )

assume that

A2: C is connected and

A3: C is open ; :: thesis: ex H being Subset of X st

( H is open & H is connected & C = E /\ H )

C in the topology of (X | E) by A3, PRE_TOPC:def 2;

then consider G being Subset of X such that

A4: G in the topology of X and

A5: C = G /\ ([#] (X | E)) by PRE_TOPC:def 4;

A6: C = G /\ E by A5, PRE_TOPC:def 5;

reconsider G = G as non empty Subset of X by A5;

A7: G is open by A4, PRE_TOPC:def 2;

reconsider C1 = C as Subset of X by PRE_TOPC:11;

C <> {} (X | E) ;

then consider x being Point of (X | E) such that

A8: x in C by PRE_TOPC:12;

x in G by A5, A8, XBOOLE_0:def 4;

then x in [#] (X | G) by PRE_TOPC:def 5;

then reconsider y = x as Point of (X | G) ;

set H1 = Component_of y;

reconsider H = Component_of y as Subset of X by PRE_TOPC:11;

take H ; :: thesis: ( H is open & H is connected & C = E /\ H )

A9: Component_of y is a_component by CONNSP_1:40;

then H is_a_component_of G by CONNSP_1:def 6;

hence H is open by A1, A7, Th18; :: thesis: ( H is connected & C = E /\ H )

C c= G by A5, XBOOLE_1:17;

then C c= [#] (X | G) by PRE_TOPC:def 5;

then reconsider C2 = C1 as Subset of (X | G) ;

Component_of y c= [#] (X | G) ;

then A10: H c= G by PRE_TOPC:def 5;

C1 is connected by A2, CONNSP_1:23;

then C2 is connected by CONNSP_1:23;

then ( C2 misses H or C2 c= H ) by A9, CONNSP_1:36;

then A11: ( C2 /\ H = {} (X | G) or C2 c= H ) by XBOOLE_0:def 7;

A12: x in Component_of y by CONNSP_1:38;

H /\ (G /\ E) c= C by A6, XBOOLE_0:def 4;

then (H /\ G) /\ E c= C by XBOOLE_1:16;

then A13: E /\ H c= C by A10, XBOOLE_1:28;

thus H is connected by CONNSP_1:23; :: thesis: C = E /\ H

C c= E by A6, XBOOLE_1:17;

then C c= E /\ H by A8, A11, A12, XBOOLE_0:def 4;

hence C = E /\ H by A13, XBOOLE_0:def 10; :: thesis: verum