let T be non empty TopSpace; :: thesis: for x being Point of T
for X being Subset of T
for K being Basis of T st ( for A being Subset of T st A in K & x in A holds
A meets X ) holds
x in Cl X
let x be Point of T; :: thesis: for X being Subset of T
for K being Basis of T st ( for A being Subset of T st A in K & x in A holds
A meets X ) holds
x in Cl X
let X be Subset of T; :: thesis: for K being Basis of T st ( for A being Subset of T st A in K & x in A holds
A meets X ) holds
x in Cl X
let BB be Basis of T; :: thesis: ( ( for A being Subset of T st A in BB & x in A holds
A meets X ) implies x in Cl X )
assume A1: for A being Subset of T st A in BB & x in A holds
A meets X ; :: thesis: x in Cl X
now :: thesis: for G being a_neighborhood of x holds G meets X
let G be a_neighborhood of x; :: thesis: G meets X
A2: Int G = union { A where A is Subset of T : ( A in BB & A c= G ) } by YELLOW_8:11;
x in Int G by CONNSP_2:def 1;
then consider Z being set such that
A3: x in Z and
A4: Z in { A where A is Subset of T : ( A in BB & A c= G ) } by A2, TARSKI:def 4;
ex A being Subset of T st
( Z = A & A in BB & A c= G ) by A4;
hence G meets X by A1, A3, XBOOLE_1:63; :: thesis: verum
end;
hence x in Cl X by CONNSP_2:27; :: thesis: verum