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 )
reconsider A = [#] S as non empty Subset of T by TSEP_1:1;
A1: A is open by TSEP_1:def 1;
assume T is locally_connected ; :: thesis: TopStruct(# the carrier of S, the topology of S #) is locally_connected
then [#] S is locally_connected by A1, Th11, CONNSP_2:17;
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 ;
hence TopStruct(# the carrier of S, the topology of S #) is locally_connected by TSEP_1:3; :: thesis: verum