theorem :: BORSUK_5:13

for A being Subset of R^1
for p being Point of RealSpace holds
( p in Cl A iff for r being Real st r > 0 holds
Ball (p,r) meets A ) by GOBOARD6:92, TOPMETR:def 6;