:: deftheorem defines cl_Ball NDIFF_8:def 1 :
for M being RealNormSpace
for p being Element of M
for r being Real holds cl_Ball (p,r) = { q where q is Element of M : ||.(p - q).|| <= r } ;