for a being Real
for r1, r2 being positive Real st r1 <= r2 holds
Ball (|[a,r1]|,r1) c= Ball (|[a,r2]|,r2)