for n being Nat
for V being Subset of (TOP-REAL n) holds
( V in the topology of (TOP-REAL n) iff for p being Point of (TOP-REAL n) st p in V holds
ex r being Real st
( r > 0 & Ball (p,r) c= V ) )