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

proof

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

end;

then X | A is locally_connected ;
hence A is locally_connected ; :: thesis: verum