let T be non empty TopSpace; :: thesis: ( ex B being Basis of T st

for X being Subset of T st X in B holds

X is connected implies T is locally_connected )

given B being Basis of T such that A1: for X being Subset of T st X in B holds

X is connected ; :: thesis: T is locally_connected

let x be Point of T; :: according to CONNSP_2:def 4 :: thesis: T is_locally_connected_in x

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

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

assume A2: x in Int U ; :: according to CONNSP_2:def 1 :: thesis: ex b_{1} being Element of bool the carrier of T st

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

( Int U in the topology of T & the topology of T c= UniCl B ) by CANTOR_1:def 2, PRE_TOPC:def 2;

then consider Y being Subset-Family of T such that

A3: Y c= B and

A4: Int U = union Y by CANTOR_1:def 1;

consider V being set such that

A5: x in V and

A6: V in Y by A2, A4, TARSKI:def 4;

reconsider V = V as Subset of T by A6;

take V ; :: thesis: ( V is a_neighborhood of x & V is connected & V c= U )

( B c= the topology of T & V in B ) by A3, A6, TOPS_2:64;

then V is open by PRE_TOPC:def 2;

hence x in Int V by A5, TOPS_1:23; :: according to CONNSP_2:def 1 :: thesis: ( V is connected & V c= U )

thus V is connected by A1, A3, A6; :: thesis: V c= U

A7: Int U c= U by TOPS_1:16;

V c= union Y by A6, ZFMISC_1:74;

hence V c= U by A4, A7; :: thesis: verum

for X being Subset of T st X in B holds

X is connected implies T is locally_connected )

given B being Basis of T such that A1: for X being Subset of T st X in B holds

X is connected ; :: thesis: T is locally_connected

let x be Point of T; :: according to CONNSP_2:def 4 :: thesis: T is_locally_connected_in x

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

( b

assume A2: x in Int U ; :: according to CONNSP_2:def 1 :: thesis: ex b

( b

( Int U in the topology of T & the topology of T c= UniCl B ) by CANTOR_1:def 2, PRE_TOPC:def 2;

then consider Y being Subset-Family of T such that

A3: Y c= B and

A4: Int U = union Y by CANTOR_1:def 1;

consider V being set such that

A5: x in V and

A6: V in Y by A2, A4, TARSKI:def 4;

reconsider V = V as Subset of T by A6;

take V ; :: thesis: ( V is a_neighborhood of x & V is connected & V c= U )

( B c= the topology of T & V in B ) by A3, A6, TOPS_2:64;

then V is open by PRE_TOPC:def 2;

hence x in Int V by A5, TOPS_1:23; :: according to CONNSP_2:def 1 :: thesis: ( V is connected & V c= U )

thus V is connected by A1, A3, A6; :: thesis: V c= U

A7: Int U c= U by TOPS_1:16;

V c= union Y by A6, ZFMISC_1:74;

hence V c= U by A4, A7; :: thesis: verum