theorem :: TOPREAL9:61

for a, b, r being Real
for s, t being Point of (TOP-REAL 2) st s in circle (a,b,r) & t in circle (a,b,r) holds
(LSeg (s,t)) /\ (circle (a,b,r)) = {s,t}