let a, b, r, w be real number ; :: thesis: for s, t being Point of (TOP-REAL 2)
for S, T, Y being Element of REAL 2 st S = ((1 / 2) * s) + ((1 / 2) * t) & T = t & Y = |[a,b]| & s <> t & s in circle a,b,r & t in closed_inside_of_circle a,b,r holds
ex e being Point of (TOP-REAL 2) st
( e <> s & {s,e} = (halfline s,t) /\ (circle a,b,r) & ( t in Sphere |[a,b]|,r implies e = t ) & ( not t in Sphere |[a,b]|,r & w = ((- (2 * |((t - (((1 / 2) * s) + ((1 / 2) * t))),((((1 / 2) * s) + ((1 / 2) * t)) - |[a,b]|))|)) + (sqrt (delta (Sum (sqr (T - S))),(2 * |((t - (((1 / 2) * s) + ((1 / 2) * t))),((((1 / 2) * s) + ((1 / 2) * t)) - |[a,b]|))|),((Sum (sqr (S - Y))) - (r ^2 ))))) / (2 * (Sum (sqr (T - S)))) implies e = ((1 - w) * (((1 / 2) * s) + ((1 / 2) * t))) + (w * t) ) )
let s, t be Point of (TOP-REAL 2); :: thesis: for S, T, Y being Element of REAL 2 st S = ((1 / 2) * s) + ((1 / 2) * t) & T = t & Y = |[a,b]| & s <> t & s in circle a,b,r & t in closed_inside_of_circle a,b,r holds
ex e being Point of (TOP-REAL 2) st
( e <> s & {s,e} = (halfline s,t) /\ (circle a,b,r) & ( t in Sphere |[a,b]|,r implies e = t ) & ( not t in Sphere |[a,b]|,r & w = ((- (2 * |((t - (((1 / 2) * s) + ((1 / 2) * t))),((((1 / 2) * s) + ((1 / 2) * t)) - |[a,b]|))|)) + (sqrt (delta (Sum (sqr (T - S))),(2 * |((t - (((1 / 2) * s) + ((1 / 2) * t))),((((1 / 2) * s) + ((1 / 2) * t)) - |[a,b]|))|),((Sum (sqr (S - Y))) - (r ^2 ))))) / (2 * (Sum (sqr (T - S)))) implies e = ((1 - w) * (((1 / 2) * s) + ((1 / 2) * t))) + (w * t) ) )
reconsider G = |[a,b]| as Point of (Euclid 2) by TOPREAL3:13;
A1: ( cl_Ball G,r = closed_inside_of_circle a,b,r & cl_Ball G,r = cl_Ball |[a,b]|,r ) by Th14, Th47;
Sphere G,r = circle a,b,r by Th49;
then A2: Sphere |[a,b]|,r = circle a,b,r by Th15;
let S, T, Y be Element of REAL 2; :: thesis: ( S = ((1 / 2) * s) + ((1 / 2) * t) & T = t & Y = |[a,b]| & s <> t & s in circle a,b,r & t in closed_inside_of_circle a,b,r implies ex e being Point of (TOP-REAL 2) st
( e <> s & {s,e} = (halfline s,t) /\ (circle a,b,r) & ( t in Sphere |[a,b]|,r implies e = t ) & ( not t in Sphere |[a,b]|,r & w = ((- (2 * |((t - (((1 / 2) * s) + ((1 / 2) * t))),((((1 / 2) * s) + ((1 / 2) * t)) - |[a,b]|))|)) + (sqrt (delta (Sum (sqr (T - S))),(2 * |((t - (((1 / 2) * s) + ((1 / 2) * t))),((((1 / 2) * s) + ((1 / 2) * t)) - |[a,b]|))|),((Sum (sqr (S - Y))) - (r ^2 ))))) / (2 * (Sum (sqr (T - S)))) implies e = ((1 - w) * (((1 / 2) * s) + ((1 / 2) * t))) + (w * t) ) ) )
assume ( S = ((1 / 2) * s) + ((1 / 2) * t) & T = t & Y = |[a,b]| & s <> t & s in circle a,b,r & t in closed_inside_of_circle a,b,r ) ; :: thesis: ex e being Point of (TOP-REAL 2) st
( e <> s & {s,e} = (halfline s,t) /\ (circle a,b,r) & ( t in Sphere |[a,b]|,r implies e = t ) & ( not t in Sphere |[a,b]|,r & w = ((- (2 * |((t - (((1 / 2) * s) + ((1 / 2) * t))),((((1 / 2) * s) + ((1 / 2) * t)) - |[a,b]|))|)) + (sqrt (delta (Sum (sqr (T - S))),(2 * |((t - (((1 / 2) * s) + ((1 / 2) * t))),((((1 / 2) * s) + ((1 / 2) * t)) - |[a,b]|))|),((Sum (sqr (S - Y))) - (r ^2 ))))) / (2 * (Sum (sqr (T - S)))) implies e = ((1 - w) * (((1 / 2) * s) + ((1 / 2) * t))) + (w * t) ) )
hence ex e being Point of (TOP-REAL 2) st
( e <> s & {s,e} = (halfline s,t) /\ (circle a,b,r) & ( t in Sphere |[a,b]|,r implies e = t ) & ( not t in Sphere |[a,b]|,r & w = ((- (2 * |((t - (((1 / 2) * s) + ((1 / 2) * t))),((((1 / 2) * s) + ((1 / 2) * t)) - |[a,b]|))|)) + (sqrt (delta (Sum (sqr (T - S))),(2 * |((t - (((1 / 2) * s) + ((1 / 2) * t))),((((1 / 2) * s) + ((1 / 2) * t)) - |[a,b]|))|),((Sum (sqr (S - Y))) - (r ^2 ))))) / (2 * (Sum (sqr (T - S)))) implies e = ((1 - w) * (((1 / 2) * s) + ((1 / 2) * t))) + (w * t) ) ) by A1, A2, Th38; :: thesis: verum