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

reconsider s = t as Point of S by A1;

let U be Subset of T; :: according to CONNSP_2:def 3 :: thesis: ( not U is a_neighborhood of t or ex b_{1} being Element of bool the carrier of T st

( b_{1} is a_neighborhood of t & b_{1} is connected & b_{1} c= U ) )

reconsider U1 = U as Subset of S by A1;

assume U is a_neighborhood of t ; :: thesis: ex b_{1} being Element of bool the carrier of T st

( b_{1} is a_neighborhood of t & b_{1} is connected & b_{1} c= U )

then A3: U1 is a_neighborhood of s by A1, Th8;

S is_locally_connected_in s by A2;

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;

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

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

reconsider s = t as Point of S by A1;

let U be Subset of T; :: according to CONNSP_2:def 3 :: thesis: ( not U is a_neighborhood of t or ex b

( b

reconsider U1 = U as Subset of S by A1;

assume U is a_neighborhood of t ; :: thesis: ex b

( b

then A3: U1 is a_neighborhood of s by A1, Th8;

S is_locally_connected_in s by A2;

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;

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