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 )

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) )

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 A9:
for A being non empty Subset of X
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;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

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

hence
X is_locally_connected_in x
by Th14; :: thesis: verum
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;( 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