let X be non empty TopSpace; :: thesis: for x being Point of X holds
( X is_locally_connected_in x iff for V, S being Subset of X st V is a_neighborhood of x & S is_a_component_of V & x in S holds
S is a_neighborhood of x )

let x be Point of X; :: thesis: ( X is_locally_connected_in x iff for V, S being Subset of X st V is a_neighborhood of x & S is_a_component_of V & x in S holds
S is a_neighborhood of x )

thus ( X is_locally_connected_in x implies for V, S being Subset of X st V is a_neighborhood of x & S is_a_component_of V & x in S holds
S is a_neighborhood of x ) :: thesis: ( ( for V, S being Subset of X st V is a_neighborhood of x & S is_a_component_of V & x in S holds
S is a_neighborhood of x ) implies X is_locally_connected_in x )
proof
assume A1: X is_locally_connected_in x ; :: thesis: for V, S being Subset of X st V is a_neighborhood of x & S is_a_component_of V & x in S holds
S is a_neighborhood of x

let V, S be Subset of X; :: thesis: ( V is a_neighborhood of x & S is_a_component_of V & x in S implies S is a_neighborhood of x )
assume that
A2: V is a_neighborhood of x and
A3: S is_a_component_of V and
A4: x in S ; :: thesis: S is a_neighborhood of x
reconsider V9 = V as non empty Subset of X by ;
consider S1 being Subset of (X | V) such that
A5: S1 = S and
A6: S1 is a_component by ;
consider V1 being Subset of X such that
A7: V1 is a_neighborhood of x and
A8: V1 is connected and
A9: V1 c= V by A1, A2;
V1 c= [#] (X | V) by ;
then reconsider V2 = V1 as Subset of (X | V) ;
A10: x in Int V1 by ;
V2 is connected by ;
then ( V2 misses S1 or V2 c= S1 ) by ;
then A11: ( V2 /\ S1 = {} (X | V9) or V2 c= S1 ) by XBOOLE_0:def 7;
x in V2 by ;
then Int V1 c= Int S by ;
hence S is a_neighborhood of x by ; :: thesis: verum
end;
assume A12: for V, S being Subset of X st V is a_neighborhood of x & S is_a_component_of V & x in S holds
S is a_neighborhood of x ; :: thesis:
for U1 being Subset of X st U1 is a_neighborhood of x holds
ex V being Subset of X st
( V is a_neighborhood of x & V is connected & V c= U1 )
proof
let U1 be Subset of X; :: thesis: ( U1 is a_neighborhood of x implies ex V being Subset of X st
( V is a_neighborhood of x & V is connected & V c= U1 ) )

A13: [#] (X | U1) = U1 by PRE_TOPC:def 5;
assume A14: U1 is a_neighborhood of x ; :: thesis: ex V being Subset of X st
( V is a_neighborhood of x & V is connected & V c= U1 )

then A15: x in U1 by Th4;
reconsider U1 = U1 as non empty Subset of X by ;
x in [#] (X | U1) by ;
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;
take S ; :: thesis: ( S is a_neighborhood of x & S is connected & S c= U1 )
Component_of x1 is a_component by CONNSP_1:40;
then A16: S is_a_component_of U1 by CONNSP_1:def 6;
( x in S & Component_of x1 is connected ) by CONNSP_1:38;
hence ( S is a_neighborhood of x & S is connected & S c= U1 ) by ; :: thesis: verum
end;
hence X is_locally_connected_in x ; :: thesis: verum