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