theorem LMBALL1X: :: NDIFF_8:16

for M being RealNormSpace
for p being Element of M
for r1, r2 being Real st r1 < r2 holds
cl_Ball (p,r1) c= Ball (p,r2)