theorem :: EUCLID_6:29

for p1, p2 being Point of (TOP-REAL 2)
for a, b, r being Real st p1 in inside_of_circle (a,b,r) & p2 in outside_of_circle (a,b,r) holds
ex p being Point of (TOP-REAL 2) st p in (LSeg (p1,p2)) /\ (circle (a,b,r)) by Lm17;