let n be Element of NAT ; :: thesis: for r being non negative Real
for s, t, x being Point of (TOP-REAL n) st s <> t & s in the carrier of (Tcircle (x,r)) & t is Point of (Tdisk (x,r)) holds
ex e being Point of (Tcircle (x,r)) st
( e <> s & {s,e} = (halfline (s,t)) /\ (Sphere (x,r)) )
let r be non negative Real; :: thesis: for s, t, x being Point of (TOP-REAL n) st s <> t & s in the carrier of (Tcircle (x,r)) & t is Point of (Tdisk (x,r)) holds
ex e being Point of (Tcircle (x,r)) st
( e <> s & {s,e} = (halfline (s,t)) /\ (Sphere (x,r)) )
let s, t, x be Point of (TOP-REAL n); :: thesis: ( s <> t & s in the carrier of (Tcircle (x,r)) & t is Point of (Tdisk (x,r)) implies ex e being Point of (Tcircle (x,r)) st
( e <> s & {s,e} = (halfline (s,t)) /\ (Sphere (x,r)) ) )
assume A1: ( s <> t & s in the carrier of (Tcircle (x,r)) & t is Point of (Tdisk (x,r)) ) ; :: thesis: ex e being Point of (Tcircle (x,r)) st
( e <> s & {s,e} = (halfline (s,t)) /\ (Sphere (x,r)) )
reconsider S = ((1 / 2) * s) + ((1 / 2) * t), T = t, X = x as Element of REAL n by EUCLID:22;
A2: the carrier of (Tcircle (x,r)) = Sphere (x,r) by TOPREALB:9;
set a = ((- (2 * |((t - (((1 / 2) * s) + ((1 / 2) * t))),((((1 / 2) * s) + ((1 / 2) * t)) - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((t - (((1 / 2) * s) + ((1 / 2) * t))),((((1 / 2) * s) + ((1 / 2) * t)) - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))));
the carrier of (Tdisk (x,r)) = cl_Ball (x,r) by Th3;
then consider e1 being Point of (TOP-REAL n) such that
A3: e1 <> s and
A4: {s,e1} = (halfline (s,t)) /\ (Sphere (x,r)) and
( t in Sphere (x,r) implies e1 = t ) and
( not t in Sphere (x,r) & ((- (2 * |((t - (((1 / 2) * s) + ((1 / 2) * t))),((((1 / 2) * s) + ((1 / 2) * t)) - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((t - (((1 / 2) * s) + ((1 / 2) * t))),((((1 / 2) * s) + ((1 / 2) * t)) - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))) = ((- (2 * |((t - (((1 / 2) * s) + ((1 / 2) * t))),((((1 / 2) * s) + ((1 / 2) * t)) - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((t - (((1 / 2) * s) + ((1 / 2) * t))),((((1 / 2) * s) + ((1 / 2) * t)) - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))) implies e1 = ((1 - (((- (2 * |((t - (((1 / 2) * s) + ((1 / 2) * t))),((((1 / 2) * s) + ((1 / 2) * t)) - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((t - (((1 / 2) * s) + ((1 / 2) * t))),((((1 / 2) * s) + ((1 / 2) * t)) - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))))) * (((1 / 2) * s) + ((1 / 2) * t))) + ((((- (2 * |((t - (((1 / 2) * s) + ((1 / 2) * t))),((((1 / 2) * s) + ((1 / 2) * t)) - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((t - (((1 / 2) * s) + ((1 / 2) * t))),((((1 / 2) * s) + ((1 / 2) * t)) - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))) * t) ) by A1, A2, TOPREAL9:38;
e1 in {s,e1} by TARSKI:def 2;
then e1 in Sphere (x,r) by A4, XBOOLE_0:def 4;
hence ex e being Point of (Tcircle (x,r)) st
( e <> s & {s,e} = (halfline (s,t)) /\ (Sphere (x,r)) ) by A2, A3, A4; :: thesis: verum