let X be non empty TopSpace; :: thesis: ( X is locally_connected iff for A being non empty Subset of X
for B being Subset of X st A is open & B is_a_component_of A holds
B is open )
thus ( X is locally_connected implies for A being non empty Subset of X
for B being Subset of X st A is open & B is_a_component_of A holds
B is open ) :: thesis: ( ( for A being non empty Subset of X
for B being Subset of X st A is open & B is_a_component_of A holds
B is open ) implies X is locally_connected )

proof

assume A1: X is locally_connected ; :: thesis: for A being non empty Subset of X
for B being Subset of X st A is open & B is_a_component_of A holds
B is open
let A be non empty Subset of X; :: thesis: for B being Subset of X st A is open & B is_a_component_of A holds
B is open
let B be Subset of X; :: thesis: ( A is open & B is_a_component_of A implies B is open )
assume that
A2: A is open and
A3: B is_a_component_of A ; :: thesis: B is open
consider B1 being Subset of (X | A) such that
A4: B1 = B and
A5: B1 is a_component by A3, CONNSP_1:def 6;
reconsider B1 = B1 as Subset of (X | A) ;
A is locally_connected by A1, A2, Th17;
then X | A is locally_connected ;
then B1 is open by A5, Th15;
then B1 in the topology of (X | A) by PRE_TOPC:def 2;
then consider B2 being Subset of X such that
A6: B2 in the topology of X and
A7: B1 = B2 /\ ([#] (X | A)) by PRE_TOPC:def 4;
A8: B = B2 /\ A by A4, A7, PRE_TOPC:def 5;
reconsider B2 = B2 as Subset of X ;
B2 is open by A6, PRE_TOPC:def 2;
hence B is open by A2, A8; :: thesis: verum

end;

assume A9: for A being non empty Subset of X
for B being Subset of X st A is open & B is_a_component_of A holds
B is open ; :: thesis: X is locally_connected
let x be Point of X; :: according to CONNSP_2:def 4 :: thesis: X is_locally_connected_in x
for U1 being non empty Subset of X st U1 is open & x in U1 holds
ex x1 being Point of (X | U1) st
( x1 = x & x in Int (Component_of x1) )

proof

let U1 be non empty Subset of X; :: thesis: ( U1 is open & x in U1 implies ex x1 being Point of (X | U1) st
( x1 = x & x in Int (Component_of x1) ) )
assume that
A10: U1 is open and
A11: x in U1 ; :: thesis: ex x1 being Point of (X | U1) st
( x1 = x & x in Int (Component_of x1) )
x in [#] (X | U1) by A11, PRE_TOPC:def 5;
then reconsider x1 = x as Point of (X | U1) ;
set S1 = Component_of x1;
reconsider S = Component_of x1 as Subset of X by PRE_TOPC:11;
Component_of x1 is a_component by CONNSP_1:40;
then S is_a_component_of U1 by CONNSP_1:def 6;
then A12: S is open by A9, A10;
take x1 ; :: thesis: ( x1 = x & x in Int (Component_of x1) )
x in S by CONNSP_1:38;
then Component_of x1 is a_neighborhood of x1 by A12, Th3, Th10;
hence ( x1 = x & x in Int (Component_of x1) ) by Def1; :: thesis: verum

end;

hence X is_locally_connected_in x by Th14; :: thesis: verum