let n be Element of NAT ; :: thesis: for r being non negative Real
for s, t, x being Point of () st s <> t & s is Point of (Tdisk (x,r)) & s is not Point of (Tcircle (x,r)) holds
ex e being Point of (Tcircle (x,r)) st {e} = (halfline (s,t)) /\ (Sphere (x,r))

let r be non negative Real; :: thesis: for s, t, x being Point of () st s <> t & s is Point of (Tdisk (x,r)) & s is not Point of (Tcircle (x,r)) holds
ex e being Point of (Tcircle (x,r)) st {e} = (halfline (s,t)) /\ (Sphere (x,r))

let s, t, x be Point of (); :: thesis: ( s <> t & s is Point of (Tdisk (x,r)) & s is not Point of (Tcircle (x,r)) implies ex e being Point of (Tcircle (x,r)) st {e} = (halfline (s,t)) /\ (Sphere (x,r)) )
assume that
A1: s <> t and
A2: s is Point of (Tdisk (x,r)) and
A3: s is not Point of (Tcircle (x,r)) ; :: thesis: ex e being Point of (Tcircle (x,r)) st {e} = (halfline (s,t)) /\ (Sphere (x,r))
reconsider S = s, T = t, X = x as Element of REAL n by EUCLID:22;
set a = ((- (2 * |((t - s),(s - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((t - s),(s - 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 A4: |.(s - x).| <= r by ;
A5: the carrier of (Tcircle (x,r)) = Sphere (x,r) by TOPREALB:9;
then |.(s - x).| <> r by ;
then |.(s - x).| < r by ;
then s in Ball (x,r) by TOPREAL9:7;
then consider e1 being Point of () such that
A6: {e1} = (halfline (s,t)) /\ (Sphere (x,r)) and
e1 = ((1 - (((- (2 * |((t - s),(s - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((t - s),(s - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))))) * s) + ((((- (2 * |((t - s),(s - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((t - s),(s - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))) * t) by ;
e1 in {e1} by TARSKI:def 1;
then e1 in Sphere (x,r) by ;
hence ex e being Point of (Tcircle (x,r)) st {e} = (halfline (s,t)) /\ (Sphere (x,r)) by A5, A6; :: thesis: verum