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

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