theorem :: TOPREAL9:60

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)) \ {s,t} c= inside_of_circle (a,b,r)