theorem Th34: :: TOPREAL9:36

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