theorem :: TOPREAL9:58

for a, b, r, w being Real
for s, t being Point of (TOP-REAL 2)
for S, T, X being Element of REAL 2 st S = s & T = t & X = |[a,b]| & w = ((- (2 * |((t - s),(s - |[a,b]|))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((t - s),(s - |[a,b]|))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))) & s <> t & s in inside_of_circle (a,b,r) holds
ex e being Point of (TOP-REAL 2) st
( {e} = (halfline (s,t)) /\ (circle (a,b,r)) & e = ((1 - w) * s) + (w * t) )