let T be non empty TopSpace; :: thesis: for x being Point of T
for X being Subset of T
for K being prebasis of T st ( for Z being finite Subset-Family of T st Z c= K & x in Intersect Z holds
Intersect Z meets X ) holds
x in Cl X
let x be Point of T; :: thesis: for X being Subset of T
for K being prebasis of T st ( for Z being finite Subset-Family of T st Z c= K & x in Intersect Z holds
Intersect Z meets X ) holds
x in Cl X
let X be Subset of T; :: thesis: for K being prebasis of T st ( for Z being finite Subset-Family of T st Z c= K & x in Intersect Z holds
Intersect Z meets X ) holds
x in Cl X
let BB be prebasis of T; :: thesis: ( ( for Z being finite Subset-Family of T st Z c= BB & x in Intersect Z holds
Intersect Z meets X ) implies x in Cl X )
assume A1: for Z being finite Subset-Family of T st Z c= BB & x in Intersect Z holds
Intersect Z meets X ; :: thesis: x in Cl X
reconsider BB9 = FinMeetCl BB as Basis of T by Th23;

now :: thesis: for A being Subset of T st A in BB9 & x in A holds
A meets X

let A be Subset of T; :: thesis: ( A in BB9 & x in A implies A meets X )
assume A in BB9 ; :: thesis: ( x in A implies A meets X )
then A2: ex Y being Subset-Family of T st
( Y c= BB & Y is finite & A = Intersect Y ) by CANTOR_1:def 3;
assume x in A ; :: thesis: A meets X
hence A meets X by A1, A2; :: thesis: verum

end;

hence x in Cl X by Th37; :: thesis: verum