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