let X be non empty TopSpace; :: thesis: ( X is locally_connected implies for A being non empty Subset of st A is open holds
A is locally_connected )
assume A1: X is locally_connected ; :: thesis: for A being non empty Subset of st A is open holds
A is locally_connected
let A be non empty Subset of ; :: thesis: ( A is open implies A is locally_connected )
assume A2: A is open ; :: thesis: A is locally_connected
for x being Point of holds X | A is_locally_connected_in x

proof

let x be Point of ; :: thesis: X | A is_locally_connected_in x
x in [#] (X | A) ;
then A3: x in A by PRE_TOPC:def 10;
then reconsider x1 = x as Point of ;
X is_locally_connected_in x1 by A1, Def4;
then A is_locally_connected_in x1 by A2, A3, Th22;
then ex x2 being Point of st
( x2 = x1 & X | A is_locally_connected_in x2 ) by Def5;
hence X | A is_locally_connected_in x ; :: thesis: verum

end;

then X | A is locally_connected by Def4;
hence A is locally_connected by Def6; :: thesis: verum