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:
let x be Point of T; :: according to CONNSP_2:def 4 :: thesis:
let U be Subset of T; :: according to CONNSP_2:def 3 :: thesis: ( not U is a_neighborhood of x or ex b1 being Element of bool the carrier of T st
( b1 is a_neighborhood of x & b1 is connected & b1 c= U ) )

assume A2: x in Int U ; :: according to CONNSP_2:def 1 :: thesis: ex b1 being Element of bool the carrier of T st
( b1 is a_neighborhood of x & b1 is connected & b1 c= U )

( Int U in the topology of T & the topology of T c= UniCl B ) by ;
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 ;
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 ;
then V is open by PRE_TOPC:def 2;
hence x in Int V by ; :: 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 ;
hence V c= U by A4, A7; :: thesis: verum