for r being Real
for N being Nat
for p1, p2 being Point of (TOP-REAL N)
for u being Point of (Euclid N) st p1 in Ball (u,r) & p2 in Ball (u,r) holds
LSeg (p1,p2) c= Ball (u,r)