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

for A being non empty Subset of X st A is open & x in A holds

A is_locally_connected_in x

let x be Point of X; :: thesis: ( X is_locally_connected_in x implies for A being non empty Subset of X st A is open & x in A holds

A is_locally_connected_in x )

assume A1: X is_locally_connected_in x ; :: thesis: for A being non empty Subset of X st A is open & x in A holds

A is_locally_connected_in x

let A be non empty Subset of X; :: thesis: ( A is open & x in A implies A is_locally_connected_in x )

assume that

A2: A is open and

A3: x in A ; :: thesis: A is_locally_connected_in x

reconsider B = A as non empty Subset of X ;

A4: [#] (X | A) = A by PRE_TOPC:def 5;

for C being non empty Subset of X st B = C holds

ex x1 being Point of (X | C) st

( x1 = x & X | C is_locally_connected_in x1 )

for A being non empty Subset of X st A is open & x in A holds

A is_locally_connected_in x

let x be Point of X; :: thesis: ( X is_locally_connected_in x implies for A being non empty Subset of X st A is open & x in A holds

A is_locally_connected_in x )

assume A1: X is_locally_connected_in x ; :: thesis: for A being non empty Subset of X st A is open & x in A holds

A is_locally_connected_in x

let A be non empty Subset of X; :: thesis: ( A is open & x in A implies A is_locally_connected_in x )

assume that

A2: A is open and

A3: x in A ; :: thesis: A is_locally_connected_in x

reconsider B = A as non empty Subset of X ;

A4: [#] (X | A) = A by PRE_TOPC:def 5;

for C being non empty Subset of X st B = C holds

ex x1 being Point of (X | C) st

( x1 = x & X | C is_locally_connected_in x1 )

proof

hence
A is_locally_connected_in x
; :: thesis: verum
let C be non empty Subset of X; :: thesis: ( B = C implies ex x1 being Point of (X | C) st

( x1 = x & X | C is_locally_connected_in x1 ) )

assume A5: B = C ; :: thesis: ex x1 being Point of (X | C) st

( x1 = x & X | C is_locally_connected_in x1 )

then reconsider y = x as Point of (X | C) by A3, A4;

take x1 = y; :: thesis: ( x1 = x & X | C is_locally_connected_in x1 )

for U1 being Subset of (X | B) st U1 is a_neighborhood of x1 holds

ex V being Subset of (X | B) st

( V is a_neighborhood of x1 & V is connected & V c= U1 )

end;( x1 = x & X | C is_locally_connected_in x1 ) )

assume A5: B = C ; :: thesis: ex x1 being Point of (X | C) st

( x1 = x & X | C is_locally_connected_in x1 )

then reconsider y = x as Point of (X | C) by A3, A4;

take x1 = y; :: thesis: ( x1 = x & X | C is_locally_connected_in x1 )

for U1 being Subset of (X | B) st U1 is a_neighborhood of x1 holds

ex V being Subset of (X | B) st

( V is a_neighborhood of x1 & V is connected & V c= U1 )

proof

hence
( x1 = x & X | C is_locally_connected_in x1 )
by A5; :: thesis: verum
let U1 be Subset of (X | B); :: thesis: ( U1 is a_neighborhood of x1 implies ex V being Subset of (X | B) st

( V is a_neighborhood of x1 & V is connected & V c= U1 ) )

assume A6: U1 is a_neighborhood of x1 ; :: thesis: ex V being Subset of (X | B) st

( V is a_neighborhood of x1 & V is connected & V c= U1 )

reconsider U2 = U1 as Subset of X by PRE_TOPC:11;

U2 is a_neighborhood of x by A2, A5, A6, Th9;

then consider V being Subset of X such that

A7: ( V is a_neighborhood of x & V is connected ) and

A8: V c= U2 by A1;

reconsider V1 = V as Subset of (X | B) by A8, XBOOLE_1:1;

take V1 ; :: thesis: ( V1 is a_neighborhood of x1 & V1 is connected & V1 c= U1 )

thus ( V1 is a_neighborhood of x1 & V1 is connected & V1 c= U1 ) by A5, A7, A8, Th10, CONNSP_1:23; :: thesis: verum

end;( V is a_neighborhood of x1 & V is connected & V c= U1 ) )

assume A6: U1 is a_neighborhood of x1 ; :: thesis: ex V being Subset of (X | B) st

( V is a_neighborhood of x1 & V is connected & V c= U1 )

reconsider U2 = U1 as Subset of X by PRE_TOPC:11;

U2 is a_neighborhood of x by A2, A5, A6, Th9;

then consider V being Subset of X such that

A7: ( V is a_neighborhood of x & V is connected ) and

A8: V c= U2 by A1;

reconsider V1 = V as Subset of (X | B) by A8, XBOOLE_1:1;

take V1 ; :: thesis: ( V1 is a_neighborhood of x1 & V1 is connected & V1 c= U1 )

thus ( V1 is a_neighborhood of x1 & V1 is connected & V1 c= U1 ) by A5, A7, A8, Th10, CONNSP_1:23; :: thesis: verum