theorem Th32: :: TOPREAL9:34

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