let X be non empty TopSpace; ( 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
; 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; 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); ( 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
; 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
; ( 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; ( 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; 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; verum