theorem :: NDIFF_8:18

for S being RealNormSpace
for p being Element of S
for r being Real holds cl_Ball (p,r) = { y where y is Point of S : ||.(y - p).|| <= r }