let a, b, w, r be real number ; :: thesis: 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); :: thesis: 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 Th50, Th52;
let S, T, X be Element of REAL 2; :: thesis: ( 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 ) ; :: thesis: 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, Th37; :: thesis: verum