let S, T be non empty TopSpace; :: thesis: ( TopStruct(# the carrier of S,the topology of S #) = TopStruct(# the carrier of T,the topology of T #) & S is locally_connected implies T is locally_connected )
assume that
A1: TopStruct(# the carrier of S,the topology of S #) = TopStruct(# the carrier of T,the topology of T #) and
A2: S is locally_connected ; :: thesis: T is locally_connected
let t be Point of T; :: according to CONNSP_2:def 4 :: thesis: T is_locally_connected_in t
let U be Subset of T; :: according to CONNSP_2:def 3 :: thesis: ( not U is a_neighborhood of t or ex b₁ being Element of bool the carrier of T st
( b₁ is a_neighborhood of t & b₁ is connected & b₁ c= U ) )
reconsider U1 = U as Subset of S by A1;
reconsider s = t as Point of S by A1;
A3: S is_locally_connected_in s by A2, CONNSP_2:def 4;
assume U is a_neighborhood of t ; :: thesis: ex b₁ being Element of bool the carrier of T st
( b₁ is a_neighborhood of t & b₁ is connected & b₁ c= U )
then U1 is a_neighborhood of s by A1, Th8;
then consider V1 being Subset of S such that
A4: V1 is a_neighborhood of s and
A5: V1 is connected and
A6: V1 c= U1 by A3, CONNSP_2:def 3;
reconsider V = V1 as Subset of T by A1;
take V ; :: thesis: ( V is a_neighborhood of t & V is connected & V c= U )
thus V is a_neighborhood of t by A1, A4, Th8; :: thesis: ( V is connected & V c= U )
thus V is connected by A1, A5, Th7; :: thesis: V c= U
thus V c= U by A6; :: thesis: verum