let n be Element of NAT ; :: thesis: for r being non negative real number
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 number ; :: 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:25;
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