let T be non empty TopSpace; :: thesis: for S being non empty open SubSpace of T st T is locally_connected holds

S is locally_connected

let S be non empty open SubSpace of T; :: thesis: ( T is locally_connected implies S is locally_connected )

assume T is locally_connected ; :: thesis: S is locally_connected

then TopStruct(# the carrier of S, the topology of S #) is locally_connected by Lm10;

hence S is locally_connected by Th12; :: thesis: verum

S is locally_connected

let S be non empty open SubSpace of T; :: thesis: ( T is locally_connected implies S is locally_connected )

assume T is locally_connected ; :: thesis: S is locally_connected

then TopStruct(# the carrier of S, the topology of S #) is locally_connected by Lm10;

hence S is locally_connected by Th12; :: thesis: verum