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