theorem :: NDIFF_8:14

for S being RealNormSpace
for p being Element of S
for r being Real st 0 < r holds
( Ball (p,r) <> {} & cl_Ball (p,r) <> {} ) by LMBALL2;