for n being Element of NAT
for a, b being Element of (TOP-REAL n)
for r1, r2 being positive Real st |.(a - b).| <= r1 - r2 holds
Ball (b,r2) c= Ball (a,r1)