for n being Nat
for p, q being Point of (TOP-REAL n)
for r, s being Real st r + |.(p - q).| <= s holds
Ball (p,r) c= Ball (q,s)