for X being RealNormSpace
for x being Point of X
for r, s being Real st r <= s holds
Ball (x,r) c= Ball (x,s)