let X be non empty TopSpace; :: thesis:
let x be Point of X; :: thesis:
assume A1: X is_locally_connected_in x ; :: thesis:
let A be non empty Subset of X; :: thesis:
assume that
A2: A is open and
A3: x in A ; :: thesis:
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 )

let C be non empty Subset of X; :: thesis:
assume A5: B = C ; :: thesis:
then reconsider y = x as Point of (X | C) by A3, A4;
take x1 = y; :: thesis:
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 )

let U1 be Subset of (X | B); :: thesis:
assume A6: U1 is a_neighborhood of x1 ; :: thesis:
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:
thus ( V1 is a_neighborhood of x1 & V1 is connected & V1 c= U1 ) by A5, A7, A8, Th10, CONNSP_1:23; :: thesis:

end;

end;