theorem :: GOBOARD6:93

for n being Nat
for A being Subset of (TOP-REAL n)
for p being Point of (TOP-REAL n)
for p9 being Point of (Euclid n) st p = p9 holds
for s being Real st s > 0 holds
( p in Cl A iff for r being Real st 0 < r & r < s holds
Ball (p9,r) meets A )