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) ) )
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 that
A1: ( S = ((1 / 2) * s) + ((1 / 2) * t) & T = t & Y = |[a,b]| ) and
A2: s <> t and
A3: s in circle a,b,r and
A4: 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) ) )
reconsider G = |[a,b]| as Point of (Euclid 2) by TOPREAL3:13;
A5: cl_Ball G,r = closed_inside_of_circle a,b,r by Th47;
A6: cl_Ball G,r = cl_Ball |[a,b]|,r by Th14;
Sphere G,r = circle a,b,r by Th49;
then Sphere |[a,b]|,r = circle a,b,r by Th15;
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, A3, A4, A5, A6, Th38; :: thesis: verum