theorem Th36: :: TOPREAL9:38

for n being Nat
for a, r being Real
for y, z, x being Point of (TOP-REAL n)
for S, T, Y being Element of REAL n st S = ((1 / 2) * y) + ((1 / 2) * z) & T = z & Y = x & y <> z & y in Sphere (x,r) & z in cl_Ball (x,r) holds
ex e being Point of (TOP-REAL n) st
( e <> y & {y,e} = (halfline (y,z)) /\ (Sphere (x,r)) & ( z in Sphere (x,r) implies e = z ) & ( not z in Sphere (x,r) & a = ((- (2 * |((z - (((1 / 2) * y) + ((1 / 2) * z))),((((1 / 2) * y) + ((1 / 2) * z)) - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - (((1 / 2) * y) + ((1 / 2) * z))),((((1 / 2) * y) + ((1 / 2) * z)) - x))|),((Sum (sqr (S - Y))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))) implies e = ((1 - a) * (((1 / 2) * y) + ((1 / 2) * z))) + (a * z) ) )