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 )

S is a_neighborhood of x ; :: thesis: X is_locally_connected_in x

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 )

( 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 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
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 A2, Th4;

consider S1 being Subset of (X | V) such that

A5: S1 = S and

A6: S1 is a_component by A3, CONNSP_1:def 6;

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

then reconsider V2 = V1 as Subset of (X | V) ;

A10: x in Int V1 by A7, Def1;

V2 is connected by A8, CONNSP_1:23;

then ( V2 misses S1 or V2 c= S1 ) by A6, CONNSP_1:36;

then A11: ( V2 /\ S1 = {} (X | V9) or V2 c= S1 ) by XBOOLE_0:def 7;

x in V2 by A7, Th4;

then Int V1 c= Int S by A4, A5, A11, TOPS_1:19, XBOOLE_0:def 4;

hence S is a_neighborhood of x by A10, Def1; :: thesis: verum

end;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 A2, Th4;

consider S1 being Subset of (X | V) such that

A5: S1 = S and

A6: S1 is a_component by A3, CONNSP_1:def 6;

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

then reconsider V2 = V1 as Subset of (X | V) ;

A10: x in Int V1 by A7, Def1;

V2 is connected by A8, CONNSP_1:23;

then ( V2 misses S1 or V2 c= S1 ) by A6, CONNSP_1:36;

then A11: ( V2 /\ S1 = {} (X | V9) or V2 c= S1 ) by XBOOLE_0:def 7;

x in V2 by A7, Th4;

then Int V1 c= Int S by A4, A5, A11, TOPS_1:19, XBOOLE_0:def 4;

hence S is a_neighborhood of x by A10, Def1; :: thesis: verum

S is a_neighborhood of x ; :: thesis: X is_locally_connected_in x

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

hence
X is_locally_connected_in x
; :: thesis: verum
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 A14, Th4;

x in [#] (X | U1) by A15, 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;

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 A12, A14, A13, A16, CONNSP_1:23; :: thesis: verum

end;( 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 A14, Th4;

x in [#] (X | U1) by A15, 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;

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 A12, A14, A13, A16, CONNSP_1:23; :: thesis: verum