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

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