theorem Th33: :: TOPREAL9:35

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