let T be non empty TopSpace; :: thesis: ( T is locally_connected iff [#] T is locally_connected )
T is SubSpace of T by TSEP_1:2;
then A1: TopStruct(# the carrier of T, the topology of T #) = TopStruct(# the carrier of (T | ([#] T)), the topology of (T | ([#] T)) #) by PRE_TOPC:8, TSEP_1:5;
hence ( T is locally_connected implies [#] T is locally_connected ) by Th12; :: thesis: ( [#] T is locally_connected implies T is locally_connected )
assume [#] T is locally_connected ; :: thesis: T is locally_connected
then T | ([#] T) is locally_connected ;
hence T is locally_connected by A1, Th12; :: thesis: verum