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:29, TSEP_1:5;

hereby :: 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 by A1, Th12;
hence [#] T is locally_connected by CONNSP_2:def 6; :: thesis: verum

end;

assume [#] T is locally_connected ; :: thesis: T is locally_connected
then T | ([#] T) is locally_connected by CONNSP_2:def 6;
hence T is locally_connected by A1, Th12; :: thesis: verum