let X be non empty TopSpace; :: thesis: for x being Point of X holds

( X is_locally_connected_in x iff 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) ) )

let x be Point of X; :: thesis: ( X is_locally_connected_in x iff 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) ) )

A1: ( X is_locally_connected_in x implies 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) ) )

ex x1 being Point of (X | U1) st

( x1 = x & x in Int (Component_of x1) ) ) implies X is_locally_connected_in x )

ex x1 being Point of (X | U1) st

( x1 = x & x in Int (Component_of x1) ) ) by A1; :: thesis: verum

( X is_locally_connected_in x iff 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) ) )

let x be Point of X; :: thesis: ( X is_locally_connected_in x iff 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) ) )

A1: ( X is_locally_connected_in x implies 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

( ( for U1 being non empty Subset of X st U1 is open & x in U1 holds
assume A2:
X is_locally_connected_in x
; :: thesis: 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) )

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

A3: U1 is open and

A4: 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 A4, PRE_TOPC:def 5;

then reconsider x1 = x as Point of (X | U1) ;

reconsider S1 = Component_of x1 as Subset of (X | U1) ;

take x1 ; :: thesis: ( x1 = x & x in Int (Component_of x1) )

reconsider S = S1 as Subset of X by PRE_TOPC:11;

A5: x in S by CONNSP_1:38;

S1 is a_component by CONNSP_1:40;

then A6: S is_a_component_of U1 by CONNSP_1:def 6;

U1 is a_neighborhood of x by A3, A4, Th3;

then S is a_neighborhood of x by A2, A6, A5, Th13;

then S1 is a_neighborhood of x1 by Th10;

hence ( x1 = x & x in Int (Component_of x1) ) by Def1; :: thesis: verum

end;ex x1 being Point of (X | U1) st

( x1 = x & x in Int (Component_of x1) )

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

A3: U1 is open and

A4: 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 A4, PRE_TOPC:def 5;

then reconsider x1 = x as Point of (X | U1) ;

reconsider S1 = Component_of x1 as Subset of (X | U1) ;

take x1 ; :: thesis: ( x1 = x & x in Int (Component_of x1) )

reconsider S = S1 as Subset of X by PRE_TOPC:11;

A5: x in S by CONNSP_1:38;

S1 is a_component by CONNSP_1:40;

then A6: S is_a_component_of U1 by CONNSP_1:def 6;

U1 is a_neighborhood of x by A3, A4, Th3;

then S is a_neighborhood of x by A2, A6, A5, Th13;

then S1 is a_neighborhood of x1 by Th10;

hence ( x1 = x & x in Int (Component_of x1) ) by Def1; :: thesis: verum

ex x1 being Point of (X | U1) st

( x1 = x & x in Int (Component_of x1) ) ) implies X is_locally_connected_in x )

proof

hence
( X is_locally_connected_in x iff for U1 being non empty Subset of X st U1 is open & x in U1 holds
assume A7:
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) ) ; :: thesis: X is_locally_connected_in x

for U1 being Subset of X st U1 is a_neighborhood of x holds

ex V1 being Subset of X st

( V1 is a_neighborhood of x & V1 is connected & V1 c= U1 )

end;ex x1 being Point of (X | U1) st

( x1 = x & x in Int (Component_of x1) ) ; :: thesis: X is_locally_connected_in x

for U1 being Subset of X st U1 is a_neighborhood of x holds

ex V1 being Subset of X st

( V1 is a_neighborhood of x & V1 is connected & V1 c= U1 )

proof

hence
X is_locally_connected_in x
; :: thesis: verum
let U1 be Subset of X; :: thesis: ( U1 is a_neighborhood of x implies ex V1 being Subset of X st

( V1 is a_neighborhood of x & V1 is connected & V1 c= U1 ) )

assume U1 is a_neighborhood of x ; :: thesis: ex V1 being Subset of X st

( V1 is a_neighborhood of x & V1 is connected & V1 c= U1 )

then consider V being non empty Subset of X such that

A8: V is a_neighborhood of x and

A9: V is open and

A10: V c= U1 by Th5;

consider x1 being Point of (X | V) such that

A11: x1 = x and

A12: x in Int (Component_of x1) by A7, A8, A9, Th4;

set S1 = Component_of x1;

reconsider S = Component_of x1 as Subset of X by PRE_TOPC:11;

take S ; :: thesis: ( S is a_neighborhood of x & S is connected & S c= U1 )

Component_of x1 c= [#] (X | V) ;

then A13: ( Component_of x1 is connected & S c= V ) by PRE_TOPC:def 5;

Component_of x1 is a_neighborhood of x1 by A11, A12, Def1;

hence ( S is a_neighborhood of x & S is connected & S c= U1 ) by A9, A10, A11, A13, Th9, CONNSP_1:23; :: thesis: verum

end;( V1 is a_neighborhood of x & V1 is connected & V1 c= U1 ) )

assume U1 is a_neighborhood of x ; :: thesis: ex V1 being Subset of X st

( V1 is a_neighborhood of x & V1 is connected & V1 c= U1 )

then consider V being non empty Subset of X such that

A8: V is a_neighborhood of x and

A9: V is open and

A10: V c= U1 by Th5;

consider x1 being Point of (X | V) such that

A11: x1 = x and

A12: x in Int (Component_of x1) by A7, A8, A9, Th4;

set S1 = Component_of x1;

reconsider S = Component_of x1 as Subset of X by PRE_TOPC:11;

take S ; :: thesis: ( S is a_neighborhood of x & S is connected & S c= U1 )

Component_of x1 c= [#] (X | V) ;

then A13: ( Component_of x1 is connected & S c= V ) by PRE_TOPC:def 5;

Component_of x1 is a_neighborhood of x1 by A11, A12, Def1;

hence ( S is a_neighborhood of x & S is connected & S c= U1 ) by A9, A10, A11, A13, Th9, CONNSP_1:23; :: thesis: verum

ex x1 being Point of (X | U1) st

( x1 = x & x in Int (Component_of x1) ) ) by A1; :: thesis: verum