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