theorem Th31: :: TOPREAL9:33

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 Ball (x,r) holds
(LSeg (y,z)) /\ (Sphere (x,r)) = {y}