let a, b, r, w be 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) )
let s, t be 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) )
A1:
( Ball (|[a,b]|,r) = inside_of_circle (a,b,r) & Sphere (|[a,b]|,r) = circle (a,b,r) )
by Th48, Th50;
let S, T, X be Element of REAL 2; ( 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) implies ex e being Point of (TOP-REAL 2) st
( {e} = (halfline (s,t)) /\ (circle (a,b,r)) & e = ((1 - w) * s) + (w * t) ) )
assume
( 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) )
; ex e being Point of (TOP-REAL 2) st
( {e} = (halfline (s,t)) /\ (circle (a,b,r)) & e = ((1 - w) * s) + (w * t) )
hence
ex e being Point of (TOP-REAL 2) st
( {e} = (halfline (s,t)) /\ (circle (a,b,r)) & e = ((1 - w) * s) + (w * t) )
by A1, Th35; verum