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 )
A3: Int U in the topology of T by PRE_TOPC:def 5;
the topology of T c= UniCl B by CANTOR_1:def 2;
then consider Y being Subset-Family of T such that
A4: Y c= B and
A5: Int U = union Y by A3, CANTOR_1:def 1;
consider V being set such that
A6: x in V and
A7: V in Y by A2, A5, TARSKI:def 4;
reconsider V = V as Subset of T by A7;
take V ; :: thesis: ( V is a_neighborhood of x & V is connected & V c= U )
A8: B c= the topology of T by CANTOR_1:def 2;
V in B by A4, A7;
then V is open by A8, PRE_TOPC:def 5;
hence x in Int V by A6, TOPS_1:55; :: according to CONNSP_2:def 1 :: thesis: ( V is connected & V c= U )
thus V is connected by A1, A4, A7; :: thesis: V c= U
A9: V c= union Y by A7, ZFMISC_1:92;
Int U c= U by TOPS_1:44;
hence V c= U by A5, A9, XBOOLE_1:1; :: thesis: verum