theorem LMBALL: :: NDIFF_8:17

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