for T being non empty TopStruct
for A being Subset of T
for p being Point of T holds
( p in Cl A iff ex K being Basis of st
for Q being Subset of T st Q in K holds
A meets Q )