for r being Real
for n being Element of NAT
for x, y being Point of (TOP-REAL n) st y in Sphere (x,r) holds
(LSeg (x,y)) \ {x,y} c= Ball (x,r)