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

hence A is locally_connected ; :: thesis: verum

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

then
X | A is locally_connected
;
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;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

hence A is locally_connected ; :: thesis: verum