for S being RealNormSpace
for p being Element of S
for r being Real st 0 < r holds
Ball (p,r) is Neighbourhood of p