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 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 (TOP-REAL n) 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 (TOP-REAL n); :: 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 A2, TOPREAL9:8;

A5: the carrier of (Tcircle (x,r)) = Sphere (x,r) by TOPREALB:9;

then |.(s - x).| <> r by A3, TOPREAL9:9;

then |.(s - x).| < r by A4, XXREAL_0:1;

then s in Ball (x,r) by TOPREAL9:7;

then consider e1 being Point of (TOP-REAL n) 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 A1, TOPREAL9:37;

e1 in {e1} by TARSKI:def 1;

then e1 in Sphere (x,r) by A6, XBOOLE_0:def 4;

hence ex e being Point of (Tcircle (x,r)) st {e} = (halfline (s,t)) /\ (Sphere (x,r)) by A5, A6; :: thesis: verum

for s, t, x being Point of (TOP-REAL n) 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 (TOP-REAL n) 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 (TOP-REAL n); :: 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 A2, TOPREAL9:8;

A5: the carrier of (Tcircle (x,r)) = Sphere (x,r) by TOPREALB:9;

then |.(s - x).| <> r by A3, TOPREAL9:9;

then |.(s - x).| < r by A4, XXREAL_0:1;

then s in Ball (x,r) by TOPREAL9:7;

then consider e1 being Point of (TOP-REAL n) 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 A1, TOPREAL9:37;

e1 in {e1} by TARSKI:def 1;

then e1 in Sphere (x,r) by A6, XBOOLE_0:def 4;

hence ex e being Point of (Tcircle (x,r)) st {e} = (halfline (s,t)) /\ (Sphere (x,r)) by A5, A6; :: thesis: verum