for a, b, r being Real
for P, Q, R being Element of (TOP-REAL 2) st Q in LSeg (P,R) & P in inside_of_circle (a,b,r) & R in inside_of_circle (a,b,r) holds
Q in inside_of_circle (a,b,r)