theorem
for
a,
b,
r,
w being
Real 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) ) )