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