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₁ being Element of bool the carrier of T st
( b₁ is a_neighborhood of x & b₁ is connected & b₁ c= U ) )
assume A2: x in Int U ; :: according to CONNSP_2:def 1 :: thesis: ex b₁ being Element of bool the carrier of T st
( b₁ is a_neighborhood of x & b₁ is connected & b₁ 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