let T be non empty TopSpace; :: thesis: for S being non empty open SubSpace of T st T is locally_connected holds
TopStruct(# the carrier of S,the topology of S #) is locally_connected
let S be non empty open SubSpace of T; :: thesis: ( T is locally_connected implies TopStruct(# the carrier of S,the topology of S #) is locally_connected )
assume A1: T is locally_connected ; :: thesis: TopStruct(# the carrier of S,the topology of S #) is locally_connected
reconsider A = [#] S as non empty Subset of T by TSEP_1:1;
A is open by TSEP_1:def 1;
then [#] S is locally_connected by A1, Th11, CONNSP_2:23;
then S is locally_connected by Th13;
then TopStruct(# the carrier of S,the topology of S #) is locally_connected by Th12;
then [#] TopStruct(# the carrier of S,the topology of S #) is locally_connected by Th13;
then TopStruct(# the carrier of S,the topology of S #) | ([#] TopStruct(# the carrier of S,the topology of S #)) is locally_connected by CONNSP_2:def 6;
hence TopStruct(# the carrier of S,the topology of S #) is locally_connected by TSEP_1:3; :: thesis: verum