theorem :: TOPREAL9:59

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