:: Intersections of Intervals and Balls in TOP-REAL n
::  by Artur Korni{\l}owicz and Yasunari Shidama
::
:: Received May 10, 2004
:: Copyright (c) 2004-2019 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NUMBERS, SUBSET_1, PRE_TOPC, EUCLID, ARYTM_1, ARYTM_3, SUPINF_2,
      XBOOLE_0, JORDAN2C, RELAT_1, CARD_1, VALUED_0, FINSEQ_1, COMPLEX1,
      SQUARE_1, CARD_3, RVSUM_1, XXREAL_0, METRIC_1, NAT_1, TARSKI, STRUCT_0,
      REAL_1, RCOMP_1, XXREAL_2, CONVEX1, RLTOPSP1, FUNCT_1, UNIALG_1,
      MSSUBFAM, FUNCOP_1, ORDINAL2, JGRAPH_2, MCART_1, PROB_1, FINSEQ_2,
      FUNCT_3, POLYEQ_1, JGRAPH_6, XCMPLX_0, RLVECT_1, INCSP_1, PENCIL_1;
 notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, RELSET_1, FUNCT_2, NUMBERS,
      XCMPLX_0, XXREAL_0, XREAL_0, COMPLEX1, REAL_1, FINSEQ_1, FINSEQ_2,
      RVSUM_1, VALUED_0, SQUARE_1, QUIN_1, POLYEQ_1, STRUCT_0, PRE_TOPC,
      METRIC_1, TBSP_1, RLVECT_1, RLTOPSP1, EUCLID, JGRAPH_2, JGRAPH_6,
      VECTSP_1;
 constructors REAL_1, SQUARE_1, BINOP_2, COMPLEX1, QUIN_1, FINSEQOP, POLYEQ_1,
      BORSUK_1, TBSP_1, MONOID_0, JGRAPH_2, JGRAPH_6, CONVEX1, GRCAT_1;
 registrations XBOOLE_0, XXREAL_0, XREAL_0, SQUARE_1, NAT_1, STRUCT_0,
      MONOID_0, EUCLID, TOPALG_2, VALUED_0, FINSEQ_1, FUNCT_1, RELAT_1,
      PRE_TOPC, TBSP_1, JORDAN2C, QUIN_1, ORDINAL1, RLTOPSP1, CARD_1;
 requirements NUMERALS, BOOLE, SUBSET, ARITHM, REAL;
 definitions TARSKI, XBOOLE_0, RLTOPSP1, JORDAN1, VECTSP_1;
 equalities RLTOPSP1, SQUARE_1, EUCLID, XCMPLX_0, ALGSTR_0, STRUCT_0;
 expansions TARSKI, XBOOLE_0, RLTOPSP1;
 theorems JGRAPH_6, TOPRNS_1, TARSKI, SUBSET_1, FUNCT_2, EUCLID, JGRAPH_2,
      XBOOLE_1, XBOOLE_0, FUNCOP_1, JORDAN2C, JORDAN1, SQUARE_1, XCMPLX_1,
      ABSVALUE, JGRAPH_1, QUIN_1, POLYEQ_1, TOPREAL3, METRIC_1, TOPREAL6,
      RVSUM_1, EUCLID_2, GOBOARD6, REVROT_1, ENUMSET1, COMPLEX1, XREAL_1,
      XXREAL_0, RLTOPSP1, RLVECT_1, VECTSP_1, RLVECT_4;

begin :: Preliminaries

reserve n for Nat,
  a, b, r, w for Real,
  x, y, z for Point of TOP-REAL n,
  e for Point of Euclid n;

::$CT 2

theorem Th1:
  n is non zero implies x <> x + 1.REAL n
proof
A1: 0.REAL n = 0.TOP-REAL n & x = x + 0.TOP-REAL n by EUCLID:66,RLVECT_1:4;
  assume that
A2: n is non zero and
A3: x = x + 1.REAL n;
   0.REAL n <> 1.REAL n by A2,REVROT_1:19;
  hence thesis by A1,A3,RLVECT_1:8;
end;

theorem Th2:
  for V being RealLinearSpace, y,z being Point of V
  for x being object holds x = (1-r)*y + r*z implies (x = y iff r = 0
  or y = z) & (x = z iff r = 1 or y = z)
proof
  let V be RealLinearSpace, y,z be Point of V;
  let x be object;
  assume
A1: x = (1-r)*y + r*z;
  hereby
    assume x = y;
    then 0.V = (1-r)*y + r*z - y by A1,RLVECT_1:5
      .= (1-r)*y - y + r*z by RLVECT_1:def 3
      .= (1-r)*y - 1 * y + r*z by RLVECT_1:def 8
      .= (1-r-1)*y + r*z by RLVECT_1:35
      .= r*z - r*y by RLVECT_1:79
      .= r*(z-y) by RLVECT_1:34;
    then r = 0 or z-y = 0.V by RLVECT_1:11;
    hence r = 0 or y = z by RLVECT_1:21;
  end;
  hereby
    assume
A2: r = 0 or y = z;
    per cases by A2;
    suppose
      r = 0;
      hence x = y + 0 * z by A1,RLVECT_1:def 8
        .= y + 0.V by RLVECT_1:10
        .= y by RLVECT_1:4;
    end;
    suppose
      z = y;
      hence x = (1-r+r)*y by A1,RLVECT_1:def 6
        .= y by RLVECT_1:def 8;
    end;
  end;
  hereby
    assume x = z;
    then 0.V = (1-r)*y + r*z - z by A1,RLVECT_1:5
      .= (1-r)*y + (r*z - z) by RLVECT_1:def 3
      .= (1-r)*y + (r*z + (-1)*z) by RLVECT_1:16
      .= (1-r)*y + (-1+r)*z by RLVECT_1:def 6
      .= (1-r)*y + (-(1-r))*z
      .= (1-r)*y - (1-r)*z by RLVECT_1:79
      .= (1-r)*(y-z) by RLVECT_1:34;
    then 1-r+r = 0+r or y-z = 0.V by RLVECT_1:11;
    hence r = 1 or y = z by RLVECT_1:21;
  end;
  assume
A3: r = 1 or y = z;
  per cases by A3;
  suppose
    r = 1;
    hence x = 0.V + 1 * z by A1,RLVECT_1:10
      .= 1 * z by RLVECT_1:4
      .= z by RLVECT_1:def 8;
  end;
  suppose
    y = z;
    hence x = (1-r+r)*z by A1,RLVECT_1:def 6
      .= z by RLVECT_1:def 8;
  end;
end;

theorem Th3:
  for f being real-valued FinSequence holds |.f.|^2 = Sum sqr f
proof
  let f be real-valued FinSequence;
  Sum sqr f >= 0 by RVSUM_1:86;
  hence thesis by SQUARE_1:def 2;
end;

theorem Th4:
  for M being non empty MetrSpace, z1, z2, z3 being Point of M st
  z1 <> z2 & z1 in cl_Ball(z3,r) & z2 in cl_Ball(z3,r) holds r > 0
proof
  let M be non empty MetrSpace, z1, z2, z3 be Point of M such that
A1: z1 <> z2 and
A2: z1 in cl_Ball(z3,r) and
A3: z2 in cl_Ball(z3,r);
  now
    assume r = 0;
    then
A4: cl_Ball(z3,r) = {z3} by TOPREAL6:56;
    then z1 = z3 by A2,TARSKI:def 1;
    hence contradiction by A1,A3,A4,TARSKI:def 1;
  end;
  hence thesis by A2,TOPREAL6:55;
end;

begin :: Subsets of TOP-REAL n

definition
  let n be Nat, x be Point of TOP-REAL n, r be Real;
  func Ball(x,r) -> Subset of TOP-REAL n equals
  {p where p is Point of
  TOP-REAL n: |. p-x .| < r};
  coherence
  proof
    {p where p is Point of TOP-REAL n: |. p-x .| < r} c= the carrier of
    TOP-REAL n
    proof
      let q be object;
      assume q in {p where p is Point of TOP-REAL n: |. p-x .| < r};
      then ex p being Point of TOP-REAL n st q = p & |. p-x .| < r;
      hence thesis;
    end;
    hence thesis;
  end;
  func cl_Ball(x,r) -> Subset of TOP-REAL n equals
  {p where p is Point of
  TOP-REAL n: |. p-x .| <= r};
  coherence
  proof
    {p where p is Point of TOP-REAL n: |. p-x .| <= r} c= the carrier of
    TOP-REAL n
    proof
      let q be object;
      assume q in {p where p is Point of TOP-REAL n: |. p-x .| <= r};
      then ex p being Point of TOP-REAL n st q = p & |. p-x .| <= r;
      hence thesis;
    end;
    hence thesis;
  end;
  func Sphere(x,r) -> Subset of TOP-REAL n equals
  {p where p is Point of
  TOP-REAL n: |. p-x .| = r};
  coherence
  proof
    {p where p is Point of TOP-REAL n: |. p-x .| = r} c= the carrier of
    TOP-REAL n
    proof
      let q be object;
      assume q in {p where p is Point of TOP-REAL n: |. p-x .| = r};
      then ex p being Point of TOP-REAL n st q = p & |. p-x .| = r;
      hence thesis;
    end;
    hence thesis;
  end;
end;

theorem Th5:
  y in Ball(x,r) iff |. y-x .| < r
proof
  hereby
    assume y in Ball(x,r);
    then ex p being Point of TOP-REAL n st y = p & |. p-x .| < r;
    hence |. y-x .| < r;
  end;
  thus thesis;
end;

theorem Th6:
  y in cl_Ball(x,r) iff |. y-x .| <= r
proof
  hereby
    assume y in cl_Ball(x,r);
    then ex p being Point of TOP-REAL n st y = p & |. p-x .| <= r;
    hence |. y-x .| <= r;
  end;
  thus thesis;
end;

theorem Th7:
  y in Sphere(x,r) iff |. y-x .| = r
proof
  hereby
    assume y in Sphere(x,r);
    then ex p being Point of TOP-REAL n st y = p & |. p-x .| = r;
    hence |. y-x .| = r;
  end;
  thus thesis;
end;

theorem
  y in Ball(0.TOP-REAL n,r) implies |.y.| < r
proof
  assume y in Ball(0.TOP-REAL n,r);
  then |. y-0.TOP-REAL n .| < r by Th5;
  hence thesis by RLVECT_1:13;
end;

theorem
  y in cl_Ball(0.TOP-REAL n,r) implies |.y.| <= r
proof
  assume y in cl_Ball(0.TOP-REAL n,r);
  then |. y-0.TOP-REAL n .| <= r by Th6;
  hence thesis by RLVECT_1:13;
end;

theorem
  y in Sphere(0.TOP-REAL n,r) implies |.y.| = r
proof
  assume y in Sphere(0.TOP-REAL n,r);
  then |. y-0.TOP-REAL n .| = r by Th7;
  hence thesis by RLVECT_1:13;
end;

theorem Th11:
  x = e implies Ball(e,r) = Ball(x,r)
proof
  assume
A1: x = e;
  hereby
    let q be object;
    assume
A2: q in Ball(e,r);
    then reconsider f = q as Point of Euclid n;
    reconsider p = f as Point of TOP-REAL n by TOPREAL3:8;
    dist(f,e) < r by A2,METRIC_1:11;
    then |. p-x .| < r by A1,JGRAPH_1:28;
    hence q in Ball(x,r);
  end;
  let q be object;
  assume
A3: q in Ball(x,r);
  then reconsider q as Point of TOP-REAL n;
  reconsider f = q as Point of Euclid n by TOPREAL3:8;
  |. q-x .| < r by A3,Th5;
  then dist(f,e) < r by A1,JGRAPH_1:28;
  hence thesis by METRIC_1:11;
end;

theorem Th12:
  x = e implies cl_Ball(e,r) = cl_Ball(x,r)
proof
  assume
A1: x = e;
  hereby
    let q be object;
    assume
A2: q in cl_Ball(e,r);
    then reconsider f = q as Point of Euclid n;
    reconsider p = f as Point of TOP-REAL n by TOPREAL3:8;
    dist(f,e) <= r by A2,METRIC_1:12;
    then |. p-x .| <= r by A1,JGRAPH_1:28;
    hence q in cl_Ball(x,r);
  end;
  let q be object;
  assume
A3: q in cl_Ball(x,r);
  then reconsider q as Point of TOP-REAL n;
  reconsider f = q as Point of Euclid n by TOPREAL3:8;
  |. q-x .| <= r by A3,Th6;
  then dist(f,e) <= r by A1,JGRAPH_1:28;
  hence thesis by METRIC_1:12;
end;

theorem Th13:
  x = e implies Sphere(e,r) = Sphere(x,r)
proof
  assume
A1: x = e;
  hereby
    let q be object;
    assume
A2: q in Sphere(e,r);
    then reconsider f = q as Point of Euclid n;
    reconsider p = f as Point of TOP-REAL n by TOPREAL3:8;
    dist(f,e) = r by A2,METRIC_1:13;
    then |. p-x .| = r by A1,JGRAPH_1:28;
    hence q in Sphere(x,r);
  end;
  let q be object;
  assume
A3: q in Sphere(x,r);
  then reconsider q as Point of TOP-REAL n;
  reconsider f = q as Point of Euclid n by TOPREAL3:8;
  |. q-x .| = r by A3,Th7;
  then dist(f,e) = r by A1,JGRAPH_1:28;
  hence thesis by METRIC_1:13;
end;

theorem
  Ball(x,r) c= cl_Ball(x,r)
proof
  reconsider e = x as Point of Euclid n by TOPREAL3:8;
  Ball(x,r) = Ball(e,r) & cl_Ball(x,r) = cl_Ball(e,r) by Th11,Th12;
  hence thesis by METRIC_1:14;
end;

theorem Th15:
  Sphere(x,r) c= cl_Ball(x,r)
proof
  reconsider e = x as Point of Euclid n by TOPREAL3:8;
  Sphere(x,r) = Sphere(e,r) & cl_Ball(x,r) = cl_Ball(e,r) by Th12,Th13;
  hence thesis by METRIC_1:15;
end;

theorem Th16:
  Ball(x,r) \/ Sphere(x,r) = cl_Ball(x,r)
proof
  reconsider e = x as Point of Euclid n by TOPREAL3:8;
A1: cl_Ball(x,r) = cl_Ball(e,r) by Th12;
  Sphere(x,r) = Sphere(e,r) & Ball(x,r) = Ball(e,r) by Th11,Th13;
  hence thesis by A1,METRIC_1:16;
end;

theorem Th17:
  Ball(x,r) misses Sphere(x,r)
proof
  assume not thesis;
  then consider q being object such that
A1: q in Ball(x,r) and
A2: q in Sphere(x,r) by XBOOLE_0:3;
  reconsider q as Point of TOP-REAL n by A1;
  |. q - x .| = r by A2,Th7;
  hence thesis by A1,Th5;
end;

registration
  let n be Nat, x be Point of TOP-REAL n;
  let r be non positive Real;
  cluster Ball(x,r) -> empty;
  coherence
  proof
    assume not thesis;
    then consider y being Point of TOP-REAL n such that
A1: y in Ball(x,r);
    |. y - x .| < r by A1,Th5;
    hence contradiction;
  end;
end;

registration
  let n be Nat, x be Point of TOP-REAL n;
  let r be positive Real;
  cluster Ball(x,r) -> non empty;
  coherence
  proof
    reconsider e = x as Point of Euclid n by TOPREAL3:8;
    Ball(x,r) = Ball(e,r) by Th11;
    hence thesis by GOBOARD6:1;
  end;
end;

theorem
  Ball(x,r) is non empty implies r > 0;

theorem
  Ball(x,r) is empty implies r <= 0;

registration
  let n be Nat, x be Point of TOP-REAL n;
  let r be negative Real;
  cluster cl_Ball(x,r) -> empty;
  coherence
  proof
    assume not thesis;
    then consider y being Point of TOP-REAL n such that
A1: y in cl_Ball(x,r);
    |. y - x .| <= r by A1,Th6;
    hence contradiction;
  end;
end;

registration
  let n be Nat, x be Point of TOP-REAL n;
  let r be non negative Real;
  cluster cl_Ball(x,r) -> non empty;
  coherence
  proof
    |. x-x .| = 0 by TOPRNS_1:28;
    hence thesis by Th6;
  end;
end;

theorem
  cl_Ball(x,r) is non empty implies r >= 0;

theorem
  cl_Ball(x,r) is empty implies r < 0;

theorem Th22:
  a + b = 1 & |.a.| + |.b.| = 1 & b <> 0 & x in cl_Ball(z,r) & y
  in Ball(z,r) implies a * x + b * y in Ball(z,r)
proof
  assume that
A1: a + b = 1 and
A2: |.a.| + |.b.| = 1 and
A3: b <> 0 and
A4: x in cl_Ball(z,r) and
A5: y in Ball(z,r);
  |. y-z .| < r by A5,Th5;
  then
A6: |. z-y .| < r by TOPRNS_1:27;
  |. x-z .| <= r by A4,Th6;
  then 0 <= |.a.| & |. z-x .| <= r by COMPLEX1:46,TOPRNS_1:27;
  then
A7: |.a.|*|. z-x .| <= |.a.|*r by XREAL_1:64;
  0 < |.b.| by A3,COMPLEX1:47;
  then |.b.|*|. z-y .| < |.b.|*r by A6,XREAL_1:68;
  then |.a.|*|. z-x .| + |.b.|*|. z-y .| < |.a.|*r + |.b.|*r by A7,XREAL_1:8;
  then a is Real & |.a.|*|. z-x .| + |.b.|*|. z-y .| < (|.a.|+|.b.|)*r;
  then b is Real & |. a*(z-x) .| + |.b.|*|. z-y .| < 1 * r by A2,TOPRNS_1:7;
  then
A8: |. a*(z-x) .| + |. b*(z-y) .| < r by TOPRNS_1:7;
  |. a*z + b*z - (a*x + b*y) .| = |. a*z - (a*x + b*y) + b*z .| by
RLVECT_1:def 3
    .= |. a*z - a*x - b*y + b*z .| by RLVECT_1:27
    .= |. a*z - a*x + b*z - b*y .| by RLVECT_1:def 3
    .= |. a*z - a*x + (b*z - b*y) .| by RLVECT_1:def 3
    .= |. a*(z-x) + (b*z - b*y) .| by RLVECT_1:34
    .= |. a*(z-x) + b*(z-y) .| by RLVECT_1:34;
  then |. a*z + b*z - (a*x + b*y) .| <= |. a*(z-x) .| + |. b*(z-y) .| by
TOPRNS_1:29;
  then |. a*z + b*z - (a*x + b*y) .| < r by A8,XXREAL_0:2;
  then
A9: |. a*x + b*y - (a*z + b*z) .| < r by TOPRNS_1:27;
  a*z + b*z = (a+b)*z by RLVECT_1:def 6
    .= z by A1,RLVECT_1:def 8;
  hence thesis by A9;
end;

registration
  let n be Nat, x be Point of TOP-REAL n;
  let r;
  cluster Ball(x,r) -> open;
  coherence
  proof
    reconsider e = x as Point of Euclid n by TOPREAL3:8;
    Ball(e,r) = Ball(x,r) by Th11;
    hence thesis by GOBOARD6:3;
  end;
  cluster cl_Ball(x,r) -> closed;
  coherence
  proof
    reconsider e = x as Point of Euclid n by TOPREAL3:8;
    cl_Ball(e,r) is bounded & cl_Ball(e,r) = cl_Ball(x,r)
    by Th12,TOPREAL6:59;
    hence thesis by TOPREAL6:58;
  end;
  cluster Sphere(x,r) -> closed;
  coherence
  proof
    reconsider e = x as Point of Euclid n by TOPREAL3:8;
    Sphere(e,r) is bounded & Sphere(e,r) = Sphere(x,r) by Th13,TOPREAL6:62;
    hence thesis by TOPREAL6:61;
  end;
end;

registration
  let n,x,r;
  cluster Ball(x,r) -> bounded;
  coherence
  proof
    reconsider e = x as Point of Euclid n by TOPREAL3:8;
    Ball(e,r) = Ball(x,r) by Th11;
    hence thesis by JORDAN2C:11;
  end;
  cluster cl_Ball(x,r) -> bounded;
  coherence
  proof
    reconsider e = x as Point of Euclid n by TOPREAL3:8;
    cl_Ball(e,r) is bounded & cl_Ball(e,r) = cl_Ball(x,r) by Th12,TOPREAL6:59;
    hence thesis by JORDAN2C:11;
  end;
  cluster Sphere(x,r) -> bounded;
  coherence
  proof
    reconsider e = x as Point of Euclid n by TOPREAL3:8;
    Sphere(e,r) is bounded & Sphere(e,r) = Sphere(x,r) by Th13,TOPREAL6:62;
    hence thesis by JORDAN2C:11;
  end;
end;

Lm1: for a being Real, P being Subset of TOP-REAL n, Q being Point of
TOP-REAL n st P = {q where q is Point of TOP-REAL n: |.q - Q.| <= a} holds P is
convex
proof
  let a be Real, P be Subset of TOP-REAL n, Q be Point of TOP-REAL n;
  assume
A1: P = {q where q is Point of TOP-REAL n: |.q - Q.| <= a};
  let p1,p2 be Point of TOP-REAL n;
  assume p1 in P;
  then
A2: ex q1 being Point of TOP-REAL n st q1=p1 & |.q1-Q.| <= a by A1;
  assume
A3: p2 in P;
  then
A4: ex q2 being Point of TOP-REAL n st q2=p2 & |.q2-Q.| <= a by A1;
  let x be object;
  assume
A5: x in LSeg(p1,p2);
  then consider r being Real such that
A6: x = (1-r)*p1+r*p2 and
A7: 0 <= r and
A8: r <= 1;
A9: r = |.r.| by A7,ABSVALUE:def 1;
  reconsider q = x as Point of TOP-REAL n by A5;
A10: |.(1-r)*(p1-Q).| = |.1-r.|*|.p1-Q.| by TOPRNS_1:7;
A11: 1-r >= 0 by A8,XREAL_1:48;
  then
A12: |.1-r.| = 1-r by ABSVALUE:def 1;
  per cases;
  suppose
A13: 1-r > 0;
    0 <= |.r.| by COMPLEX1:46;
    then
A14: |.r*(p2-Q).| = |.r.|*|.p2-Q.| & |.r.|*|.p2-Q.| <= |.r.|*a by A4,TOPRNS_1:7
,XREAL_1:64;
    (1-r)*Q + r*Q = 1 * Q - r*Q + r*Q by RLVECT_1:35
      .= 1 * Q by RLVECT_4:1
      .= Q by RLVECT_1:def 8;
    then q-Q = (1-r)*p1+r*p2-(1-r)*Q-r*Q by A6,RLVECT_1:27
      .= (1-r)*p1-(1-r)*Q+r*p2-r*Q by RLVECT_1:def 3
      .= (1-r)*(p1-Q)+r*p2-r*Q by RLVECT_1:34
      .= (1-r)*(p1-Q)+(r*p2-r*Q) by RLVECT_1:def 3
      .= (1-r)*(p1-Q)+r*(p2-Q) by RLVECT_1:34;
    then
A15: |.q-Q.| <= |.(1-r)*(p1-Q).| + |.r*(p2-Q).| by TOPRNS_1:29;
    |.1-r.|*|.p1-Q.| <= |.1-r.|*a by A2,A12,A13,XREAL_1:64;
    then |.(1-r)*(p1-Q).|+|.r*(p2-Q).| <= (1-r)*a+r*a by A9,A10,A12,A14,
XREAL_1:7;
    then |.q-Q.| <= a by A15,XXREAL_0:2;
    hence thesis by A1;
  end;
  suppose
    1-r <= 0;
    then 1-r+r = 0+r by A11;
    hence thesis by A3,A6,Th2;
  end;
end;

Lm2: for a being Real, P being Subset of TOP-REAL n, Q being Point of
TOP-REAL n st P = {q where q is Point of TOP-REAL n: |.q - Q.| < a} holds P is
convex
proof
  let a be Real, P be Subset of TOP-REAL n, Q be Point of TOP-REAL n;
  assume
A1: P = {q where q is Point of TOP-REAL n: |.q - Q.| < a};
  reconsider e = Q as Point of Euclid n by TOPREAL3:8;
  let p1,p2 be Point of TOP-REAL n;
  assume
A2: p1 in P & p2 in P;
  Ball(e,a) = Ball(Q,a) by Th11
    .= P by A1;
  hence thesis by A2,TOPREAL3:21;
end;

:: Convex subsets of TOP-REAL n

registration
  let n be Nat, x be Point of TOP-REAL n;
  let r;
  cluster Ball(x,r) -> convex;
  coherence
  by Lm2;
  cluster cl_Ball(x,r) -> convex;
  coherence
  by Lm1;
end;

definition
  let n be Nat;
  let f be Function of TOP-REAL n, TOP-REAL n;
  attr f is homogeneous means
  :Def4:
  for r being Real, x being Point of TOP-REAL n holds f.(r*x) = r * f.x;

end;

registration
  let n;
  cluster TOP-REAL n --> 0.TOP-REAL n -> homogeneous additive;
  coherence
  proof
    set f = TOP-REAL n --> 0.TOP-REAL n;
    thus f is homogeneous
    proof
      let r be Real, x be Point of TOP-REAL n;
      thus f.(r*x) = 0.TOP-REAL n by FUNCOP_1:7
        .= r * 0.TOP-REAL n by RLVECT_1:10
        .= r * f.x by FUNCOP_1:7;
    end;
    let x, y be Point of TOP-REAL n;
    thus f.(x+y) = 0.TOP-REAL n by FUNCOP_1:7
      .= 0.TOP-REAL n + 0.TOP-REAL n by RLVECT_1:4
      .= f.x + 0.TOP-REAL n by FUNCOP_1:7
      .= f.x + f.y by FUNCOP_1:7;
  end;
end;

registration
  let n;
  cluster homogeneous additive continuous for
Function of TOP-REAL n, TOP-REAL n;
  existence
  proof
    take TOP-REAL n --> 0.TOP-REAL n;
    thus thesis;
  end;
end;

registration
  let a, c be Real;
  cluster AffineMap(a,0,c,0) -> homogeneous additive;
  coherence
  proof
    set f = AffineMap(a,0,c,0);
    hereby
      let r be Real, x be Point of TOP-REAL 2;
A1:   (r*x)`1 = r*x`1 & (r*x)`2 = r*x`2 by TOPREAL3:4;
      thus f.(r*x) = |[a*((r*x)`1)+0,c*((r*x)`2)+0]| by JGRAPH_2:def 2
        .= |[r*(a*(x`1)),r*(c*(x`2))]| by A1
        .= r * |[a*(x`1)+0,c*(x`2)+0]| by EUCLID:58
        .= r * f.x by JGRAPH_2:def 2;
    end;
    let x, y be Point of TOP-REAL 2;
A2: (x+y)`1 = x`1 + y`1 & (x+y)`2 = x`2 + y`2 by TOPREAL3:2;
    thus f.(x+y) = |[a*((x+y)`1)+0,c*((x+y)`2)+0]| by JGRAPH_2:def 2
      .= |[a*(x`1)+a*(y`1),c*(x`2)+c*(y`2)]| by A2
      .= |[a*(x`1)+0,c*(x`2)+0]| + |[a*(y`1),c*(y`2)]| by EUCLID:56
      .= f.x + |[a*(y`1)+0,c*(y`2)+0]| by JGRAPH_2:def 2
      .= f.x + f.y by JGRAPH_2:def 2;
  end;
end;

theorem
  for f being homogeneous additive Function of TOP-REAL n, TOP-REAL n, X
  being convex Subset of TOP-REAL n holds f.:X is convex
proof
  let f be homogeneous additive Function of TOP-REAL n, TOP-REAL n, X be
  convex Subset of TOP-REAL n;
  let p, q be Point of TOP-REAL n;
  assume p in f.:X;
  then consider p0 being Point of TOP-REAL n such that
A1: p0 in X and
A2: p = f.p0 by FUNCT_2:65;
  assume q in f.:X;
  then consider q0 being Point of TOP-REAL n such that
A3: q0 in X and
A4: q = f.q0 by FUNCT_2:65;
A5: LSeg(p0,q0) c= X by A1,A3,JORDAN1:def 1;
  let x be object;
  assume x in LSeg(p,q);
  then consider l being Real such that
A6: x = (1-l)*p + l*q and
A7: 0 <= l & l <= 1;
  set a = (1-l)*p0 + l*q0;
A8: a in LSeg(p0,q0) by A7;
  f.a = f.((1-l)*p0) + f.(l*q0) by VECTSP_1:def 20
    .= f.((1-l)*p0) + l*f.q0 by Def4
    .= x by A2,A4,A6,Def4;
  hence thesis by A8,A5,FUNCT_2:35;
end;

:: Halflines

reserve V for RealLinearSpace,
        p,q,x for Element of V;

definition
  let V,p,q;
  func halfline(p,q) -> Subset of V equals
  { (1-l)*p + l*q where l is Real: 0 <= l };
  coherence
  proof
    set X = { (1-l)*p + l*q where l is Real: 0 <= l };
    X c= the carrier of V
    proof
      let x be object;
      assume x in X;
      then ex l being Real st x = (1-l)*p + l*q & 0 <= l;
      hence thesis;
    end;
    hence thesis;
  end;
end;

theorem
  for x being set holds x in halfline(p,q) iff ex l being Real
 st x = (1-l)*p + l*q & 0 <= l;

registration
  let V, p, q;
  cluster halfline(p,q) -> non empty;
  coherence
  proof
    (1-0)*p + 0 * q in halfline(p,q);
    hence thesis;
  end;
end;

theorem Th25:
  p in halfline(p,q)
proof
  (1-0)*p + 0 * q = p + 0 * q by RLVECT_1:def 8
    .= p + 0.V by RLVECT_1:10
    .= p by RLVECT_1:4;
  hence thesis;
end;

theorem Th26:
  q in halfline(p,q)
proof
  (1-1)*p + 1 * q = 0 * p + q by RLVECT_1:def 8
    .= 0.V + q by RLVECT_1:10
    .= q by RLVECT_1:4;
  hence thesis;
end;

theorem Th27:
  halfline(p,p) = {p}
proof
  hereby
    let d be object;
    assume d in halfline(p,p);
    then ex r being Real st d = (1-r)*p+r*p & 0 <= r;
    then d = p by Th2;
    hence d in {p} by TARSKI:def 1;
  end;
  let d be object;
  assume d in {p};
  then d = p by TARSKI:def 1;
  hence thesis by Th25;
end;

theorem Th28:
  x in halfline(p,q) implies halfline(p,x) c= halfline(p,q)
proof
  assume x in halfline(p,q);
  then consider R being Real such that
A1: x = (1-R)*p + R*q and
A2: 0 <= R;
  let d be object;
  assume
A3: d in halfline(p,x);
  then reconsider d as Point of V;
  consider r being Real such that
A4: d = (1-r)*p + r*x and
A5: 0 <= r by A3;
  set o = r*R;
  d = (1-r)*p + (r*((1-R)*p) + r*(R*q)) by A1,A4,RLVECT_1:def 5
    .= (1-r)*p + r*((1-R)*p) + r*(R*q) by RLVECT_1:def 3
    .= (1-r)*p + r*(1-R)*p + r*(R*q) by RLVECT_1:def 7
    .= ((1-r) + r*(1-R))*p + r*(R*q) by RLVECT_1:def 6
    .= (1-o)*p + o*q by RLVECT_1:def 7;
  hence thesis by A2,A5;
end;

theorem
  x in halfline(p,q) & x <> p implies halfline(p,q) = halfline(p,x)
proof
  assume
A1: x in halfline(p,q);
  then consider R being Real such that
A2: x = (1-R)*p + R*q and
A3: 0 <= R;
  assume
A4: x <> p;
  thus halfline(p,q) c= halfline(p,x)
  proof
    let d be object;
    assume
A5: d in halfline(p,q);
    then reconsider d as Point of V;
    consider r being Real such that
A6: d = (1-r)*p + r*q and
A7: 0 <= r by A5;
    set o = r/R;
    R <> 0 by A2,A4,Th2;
    then o*R = r by XCMPLX_1:87;
    then d = (1-o + o*(1-R))*p + o*(R*q) by A6,RLVECT_1:def 7
      .= (1-o)*p + o*(1-R)*p + o*(R*q) by RLVECT_1:def 6
      .= (1-o)*p + o*((1-R)*p) + o*(R*q) by RLVECT_1:def 7
      .= (1-o)*p + (o*((1-R)*p) + o*(R*q)) by RLVECT_1:def 3
      .= (1-o)*p + o*((1-R)*p + R*q) by RLVECT_1:def 5;
    hence thesis by A2,A3,A7;
  end;
  thus thesis by A1,Th28;
end;

theorem
  LSeg(p,q) c= halfline(p,q)
proof
  let a be object;
  assume a in LSeg(p,q);
  then ex r being Real st 0<=r & r<=1 & a = (1-r)*p+r*q by RLTOPSP1:76;
  hence thesis;
end;

registration
  let V, p, q;
  cluster halfline(p,q) -> convex;
  coherence
  proof
    let u, v be Point of V;
    set P = halfline(p,q);
    assume u in P;
    then consider a being Real such that
A1: u = (1-a)*p+a*q and
A2: 0 <= a;
    assume v in P;
    then consider b being Real such that
A3: v = (1-b)*p+b*q and
A4: 0 <= b;
    let x be object;
    assume x in LSeg(u,v);
    then consider r being Real such that
A5: 0 <= r and
A6: r <= 1 and
A7: x = (1-r)*u+r*v by RLTOPSP1:76;
    set o = (1-r)*a+r*b;
A8: 1-r >= r-r by A6,XREAL_1:13;
    x = (1-r)*((1-a)*p)+(1-r)*(a*q) + r*((1-b)*p+b*q) by A1,A3,A7,
RLVECT_1:def 5
      .= (1-r)*((1-a)*p) + (1-r)*(a*q) + (r*((1-b)*p) + r*(b*q)) by
RLVECT_1:def 5
      .= (1-r)*((1-a)*p) + (r*((1-b)*p) + r*(b*q)) + (1-r)*(a*q) by
RLVECT_1:def 3
      .= (1-r)*((1-a)*p) + r*((1-b)*p) + r*(b*q) + (1-r)*(a*q) by
RLVECT_1:def 3
      .= (1-r)*(1-a)*p + r*((1-b)*p) + r*(b*q) + (1-r)*(a*q) by RLVECT_1:def 7
      .= (1-r)*(1-a)*p + r*(1-b)*p + r*(b*q) + (1-r)*(a*q) by RLVECT_1:def 7
      .= (1-r)*(1-a)*p + r*(1-b)*p + r*b*q + (1-r)*(a*q) by RLVECT_1:def 7
      .= (1-r)*(1-a)*p + r*(1-b)*p + r*b*q + (1-r)*a*q by RLVECT_1:def 7
      .= ((1-r)*(1-a) + r*(1-b)) * p + r*b*q + (1-r)*a*q by RLVECT_1:def 6
      .= ((1-r)*(1-a) + r*(1-b)) * p + (r*b*q + (1-r)*a*q) by RLVECT_1:def 3
      .= (1-o)*p + o*q by RLVECT_1:def 6;
    hence thesis by A2,A4,A5,A8;
  end;
end;

reserve p, q, x for Point of TOP-REAL n;

theorem Th31:
  y in Sphere(x,r) & z in Ball(x,r) implies LSeg(y,z) /\ Sphere(x, r) = {y}
proof
  set s = y, t = z;
  assume that
A1: s in Sphere(x,r) and
A2: t in Ball(x,r);
  hereby
    let m be object;
    assume
A3: m in LSeg(s,t) /\ Sphere(x,r);
    then reconsider w = m as Point of TOP-REAL n;
    w in LSeg(s,t) by A3,XBOOLE_0:def 4;
    then consider d being Real such that
A4: 0 <= d and
A5: d <= 1 and
A6: w = (1-d)*s + d*t by RLTOPSP1:76;
A7: |. d*(t-x) .| = |.d.|*|. t-x .| by TOPRNS_1:7
      .= d*|. t-x .| by A4,ABSVALUE:def 1;
    d-1 <= 1-1 by A5,XREAL_1:9;
    then
A8: -(0 qua Element of NAT) <= -(d-1);
A9: |. (1-d)*(s-x) .| = |.1-d.|*|. s-x .| by TOPRNS_1:7
      .= (1-d)*|. s-x .| by A8,ABSVALUE:def 1
      .= (1-d)*r by A1,Th7;
    m in Sphere(x,r) by A3,XBOOLE_0:def 4;
    then
A10: r = |. w - x .| by Th7
      .= |. (1-d)*s + d*t - (1-d+d)*x .| by A6,RLVECT_1:def 8
      .= |. (1-d)*s + d*t - ((1-d)*x + d*x) .| by RLVECT_1:def 6
      .= |. (1-d)*s + d*t - (1-d)*x - d*x .| by RLVECT_1:27
      .= |. (1-d)*s - (1-d)*x + d*t - d*x .| by RLVECT_1:def 3
      .= |. (1-d)*(s-x) + d*t - d*x .| by RLVECT_1:34
      .= |. (1-d)*(s-x) + (d*t - d*x) .| by RLVECT_1:def 3
      .= |. (1-d)*(s-x) + d*(t-x) .| by RLVECT_1:34;
    per cases by A4;
    suppose
A11:  d > 0;
      |. t-x .| < r by A2,Th5;
      then d*|. t-x .| < d*r by A11,XREAL_1:68;
      then (1-d)*r + d*|. t-x .| < (1-d)*r + d*r by XREAL_1:8;
      hence m in {s} by A10,A9,A7,TOPRNS_1:29;
    end;
    suppose
      d = 0;
      then m = 1 * s + 0.TOP-REAL n by A6,RLVECT_1:10
        .= 1 * s by RLVECT_1:4
        .= s by RLVECT_1:def 8;
      hence m in {s} by TARSKI:def 1;
    end;
  end;
  let m be object;
A12: s in LSeg(s,t) by RLTOPSP1:68;
  assume m in {s};
  then m = s by TARSKI:def 1;
  hence thesis by A1,A12,XBOOLE_0:def 4;
end;

theorem Th32:
  y in Sphere(x,r) & z in Sphere(x,r) implies LSeg(y,z) \ {y,z} c= Ball(x,r)
proof
  assume that
A1: y in Sphere(x,r) and
A2: z in Sphere(x,r);
  per cases;
  suppose
    y = z;
    then LSeg(y,z) = {y} & {y,z} = {y} by ENUMSET1:29,RLTOPSP1:70;
    then LSeg(y,z) \ {y,z} = {} by XBOOLE_1:37;
    hence thesis;
  end;
  suppose
A3: y <> z;
    the carrier of TOP-REAL n = REAL n by EUCLID:22
      .= n-tuples_on REAL;
    then reconsider xf = x, yf = y, zf = z as Element of n-tuples_on REAL;
    reconsider yyf = yf, zzf = zf, xxf = xf as Element of REAL n;
    reconsider y1 = y-x, z1 = z-x as FinSequence of REAL;
    set X = |(y-x,z-x)|;
    let a be object;
A4: Sum sqr (zf-xf) = |.z1.|^2 by Th3;
A5: |. z-x .|^2 = r^2 by A2,Th7;
    assume
A6: a in LSeg(y,z) \ {y,z};
    then reconsider R = a as Point of TOP-REAL n;
A7: R in LSeg(y,z) by A6,XBOOLE_0:def 5;
    then consider l being Real such that
A8: 0 <= l and
A9: l <= 1 and
A10: R = (1-l)*y + l*z by RLTOPSP1:76;
    set l1 = 1-l;
    reconsider W1 = l1*(y-x), W2 = l*(z-x) as Element of REAL n by EUCLID:22;
A11: Sum sqr (yf-zf) >= 0 by RVSUM_1:86;
    reconsider Rf=R-x as FinSequence of REAL;
A12: W1 + W2 = l1*y-l1*x+l*(z-x) by RLVECT_1:34
      .= l1*y-l1*x+(l*z-l*x) by RLVECT_1:34
      .= l1*y-l1*x+l*z-l*x by RLVECT_1:def 3
      .= l1*y+l*z-l1*x-l*x by RLVECT_1:def 3
      .= l1*y+l*z-(l1*x+l*x) by RLVECT_1:27
      .= l1*y+l*z-(1 *x-l*x+l*x) by RLVECT_1:35
      .= l1*y+l*z-1 *x by RLVECT_4:1
      .= Rf by A10,RLVECT_1:def 8;
    reconsider W1, W2 as Element of n-tuples_on REAL;
A13: mlt(W1,W2) = (l1*mlt(yf-xf,l*(zf-xf))) by RVSUM_1:65;
A14: sqr W1 = (l1^2*sqr (yf-xf)) by RVSUM_1:58;
    Sum sqr Rf >= 0 by RVSUM_1:86;
    then |. R-x .|^2 = Sum sqr Rf by SQUARE_1:def 2
      .= Sum (sqr W1 + 2*mlt(W1,W2) + sqr W2) by A12,RVSUM_1:68
      .= Sum (sqr W1 + 2*mlt(W1,W2)) + Sum sqr W2 by RVSUM_1:89
      .= Sum sqr W1 + Sum (2*mlt(W1,W2)) + Sum sqr W2 by RVSUM_1:89
      .= l1^2*Sum sqr (yf-xf) + Sum (2*mlt(W1,W2)) + Sum sqr (l*(zf-xf)) by A14
,RVSUM_1:87
      .= l1^2*Sum sqr (yf-xf) + Sum (2*mlt(W1,W2)) + Sum (l^2*sqr (zf-xf))
    by RVSUM_1:58
      .= l1^2*Sum sqr (yf-xf) + Sum (2*mlt(W1,W2)) + l^2*Sum sqr (zf-xf) by
RVSUM_1:87
      .= l1^2*|.y1.|^2 + Sum (2*mlt(W1,W2)) + l^2*Sum sqr (zf-xf) by Th3
      .= l1^2*r^2 + Sum (2*mlt(W1,W2)) + l^2*|.z1.|^2 by A1,A4,Th7
      .= l1^2*r^2 + 2*Sum mlt(W1,W2) + l^2*r^2 by A5,RVSUM_1:87
      .= l1^2*r^2 + 2*Sum (l1*(l*mlt(yf-xf,zf-xf))) + l^2*r^2 by A13,RVSUM_1:65
      .= l1^2*r^2 + 2*Sum (l1*l*mlt(yf-xf,zf-xf)) + l^2*r^2 by RVSUM_1:49
      .= l1^2*r^2 + 2*(l1*l*Sum mlt(yf-xf,zf-xf)) + l^2*r^2 by RVSUM_1:87
      .= l1^2*r^2 + 2*l1*l*Sum mlt(yf-xf,zf-xf) + l^2*r^2
      .= l1^2*r^2 + 2*l1*l*X + l^2*r^2 by RVSUM_1:def 16
      .= (1-2*l+l^2+l^2)*r^2 + 2*l*l1*X;
    then
A15: |. R-x .|^2 - r^2 = 2*l*l1*(-r^2+X);
    now
      assume l = 0;
      then R = y by A10,Th2;
      then R in {y,z} by TARSKI:def 2;
      hence contradiction by A6,XBOOLE_0:def 5;
    end;
    then
A16: 2*l > 0 by A8,XREAL_1:129;
A17: now
      assume l1 = 0;
      then R = z by A10,Th2;
      then R in {y,z} by TARSKI:def 2;
      hence contradiction by A6,XBOOLE_0:def 5;
    end;
    1-1 <= l1 by A9,XREAL_1:13;
    then
A18: 2*l*l1 > 0 by A16,A17,XREAL_1:129;
A19: |. y-x .|^2 = r^2 by A1,Th7;
A20: now
      assume |. R-x .| = r;
      then X-r^2 = 0 by A15,A18,XCMPLX_1:6;
      then 0 = |. y-x .|^2 - 2*X + |. z-x .|^2 by A2,A19,Th7
        .= |. y-x - (z-x) .|^2 by EUCLID_2:46
        .= |. y-x-z+x .|^2 by RLVECT_1:29
        .= |. y-x+x-z .|^2 by RLVECT_1:def 3
        .= |.yf-zf.|^2 by RLVECT_4:1
        .= Sum sqr (yf-zf) by A11,SQUARE_1:def 2;
      then yf-zf = n |-> 0 by RVSUM_1:91;
      hence contradiction by A3,RVSUM_1:38;
    end;
    Sphere(x,r) c= cl_Ball(x,r) by Th15;
    then LSeg(y,z) c= cl_Ball(x,r) by A1,A2,JORDAN1:def 1;
    then |. R-x .| <= r by A7,Th6;
    then |. R-x .| < r by A20,XXREAL_0:1;
    hence thesis;
  end;
end;

theorem Th33:
  y in Sphere(x,r) & z in Sphere(x,r) implies LSeg(y,z) /\ Sphere( x,r) = {y,z}
proof
A1: y in LSeg(y,z) & z in LSeg(y,z) by RLTOPSP1:68;
  assume
A2: y in Sphere(x,r) & z in Sphere(x,r);
  then
A3: LSeg(y,z) \ {y,z} c= Ball(x,r) by Th32;
  hereby
    let a be object;
    assume
A4: a in LSeg(y,z) /\ Sphere(x,r);
    assume
A5: not a in {y,z};
    a in LSeg(y,z) by A4,XBOOLE_0:def 4;
    then
A6: a in LSeg(y,z) \ {y,z} by A5,XBOOLE_0:def 5;
A7: Ball(x,r) misses Sphere(x,r) by Th17;
    a in Sphere(x,r) by A4,XBOOLE_0:def 4;
    hence contradiction by A3,A6,A7,XBOOLE_0:3;
  end;
  let a be object;
  assume a in {y,z};
  then a = y or a = z by TARSKI:def 2;
  hence thesis by A2,A1,XBOOLE_0:def 4;
end;

theorem Th34:
  y in Sphere(x,r) & z in Sphere(x,r) implies halfline(y,z) /\
  Sphere(x,r) = {y,z}
proof
  assume that
A1: y in Sphere(x,r) and
A2: z in Sphere(x,r);
  per cases;
  suppose
A3: y = z;
    then
A4: {y,z} = {y} by ENUMSET1:29;
A5: halfline(y,z) = {y} by A3,Th27;
    hence
    for m being object st m in halfline(y,z) /\ Sphere(x,r) holds m in {y,z}
    by A4,XBOOLE_0:def 4;
    let m be object;
    assume
A6: m in {y,z};
    then m = y by A4,TARSKI:def 1;
    hence thesis by A1,A5,A4,A6,XBOOLE_0:def 4;
  end;
  suppose
A7: y <> z;
    hereby
      let m be object;
      assume
A8:   m in halfline(y,z) /\ Sphere(x,r);
      then
A9:   m in Sphere(x,r) by XBOOLE_0:def 4;
      reconsider w = m as Point of TOP-REAL n by A8;
      m in halfline(y,z) by A8,XBOOLE_0:def 4;
      then consider R being Real such that
A10:  m = (1-R)*y + R*z and
A11:  0 <= R;
      reconsider R as Real;
      per cases by A11,XXREAL_0:1;
      suppose
        R = 0;
        then m = y by A10,Th2;
        hence m in {y,z} by TARSKI:def 2;
      end;
      suppose
        R = 1;
        then m = z by A10,Th2;
        hence m in {y,z} by TARSKI:def 2;
      end;
      suppose
A12:    R > 0 & R < 1;
A13:    now
          assume m in {y,z};
          then m = y or m = z by TARSKI:def 2;
          hence contradiction by A7,A10,A12,Th2;
        end;
        w in LSeg(y,z) by A10,A12;
        then
A14:    m in LSeg(y,z) \ {y,z} by A13,XBOOLE_0:def 5;
        LSeg(y,z) \ {y,z} c= Ball(x,r) by A1,A2,Th32;
        then |. w-x .| < r by A14,Th5;
        hence m in {y,z} by A9,Th7;
      end;
      suppose
A15:    R > 1;
        then
A16:    1/R < 1 by XREAL_1:212;
A17:    (1-1/R)*y + 1/R*w = (1-1/R)*y + (1/R*((1-R)*y) + 1/R*(R*z)) by A10,
RLVECT_1:def 5
          .= (1-1/R)*y + (1/R*((1-R)*y) + 1/R*R*z) by RLVECT_1:def 7
          .= (1-1/R)*y + (1/R*((1-R)*y) + 1 * z) by A15,XCMPLX_1:87
          .= (1-1/R)*y + (1/R*((1-R)*y) + z) by RLVECT_1:def 8
          .= (1-1/R)*y + 1/R*((1-R)*y) + z by RLVECT_1:def 3
          .= (1-1/R)*y + 1/R*(1-R)*y + z by RLVECT_1:def 7
          .= (1-1/R+1/R*(1-R))*y + z by RLVECT_1:def 6
          .= (1-1/R+1/R*1-1/R*R)*y + z
          .= (1-1/R+1/R*1-1)*y + z by A15,XCMPLX_1:87
          .= 0.TOP-REAL n + z by RLVECT_1:10
          .= z by RLVECT_1:4;
A18:    now
          assume z in {y,w};
          then z = y or z = w by TARSKI:def 2;
          hence contradiction by A7,A16,A17,Th2;
        end;
        z in LSeg(y,w) by A15,A16,A17;
        then
A19:    z in LSeg(y,w) \ {y,w} by A18,XBOOLE_0:def 5;
        LSeg(y,w) \ {y,w} c= Ball(x,r) by A1,A9,Th32;
        then |. z-x .| < r by A19,Th5;
        hence m in {y,z} by A2,Th7;
      end;
    end;
    let m be object;
    assume m in {y,z};
    then
A20: m = y or m = z by TARSKI:def 2;
    y in halfline(y,z) & z in halfline(y,z) by Th25,Th26;
    hence thesis by A1,A2,A20,XBOOLE_0:def 4;
  end;
end;

theorem Th35:
  for S, T, X being Element of REAL n st S = y & T = z & X = x
holds y <> z & y in Ball(x,r) & a = (-(2*|(z-y,y-x)|) +
  sqrt delta (Sum sqr (T- S), 2 * |(z-y,y-x)|, Sum sqr (S-X) - r^2))
    / (2 * Sum sqr (T-S)) implies ex e
being Point of TOP-REAL n st {e} = halfline(y,z) /\ Sphere(x,r) & e = (1-a)*y +
  a*z
proof
  let S, T, X be Element of REAL n such that
A1: S = y and
A2: T = z and
A3: X = x;
  set s = y, t = z;
A4: Sum sqr (T-S) >= 0 by RVSUM_1:86;
  then
A5: |. T-S .|^2 = Sum sqr (T-S) by SQUARE_1:def 2;
  set A = Sum sqr (T-S);
  assume that
A6: s <> t and
A7: s in Ball(x,r) and
A8: a = (-(2*|(z-y,y-x)|) + sqrt delta (Sum sqr (T-S), 2 * |(z-y,y-x)|,
  Sum sqr (S-X) - r^2)) / (2 * Sum sqr (T-S));
A9: |. T-S .| <> 0 by A1,A2,A6,EUCLID:16;
A10: now
    assume A <= 0;
    then A = 0 by RVSUM_1:86;
    hence contradiction by A9,SQUARE_1:17;
  end;
  set C = Sum sqr (S-X) - r^2;
  set B = 2 * |(t-s,s-x)|;
A11: r = 0 or r <> 0;
  Sum sqr (S-X) >= 0 by RVSUM_1:86;
  then
A12: |. S-X .|^2 = Sum sqr (S-X) by SQUARE_1:def 2;
  |. s-x .| < r by A7,Th5;
  then (sqrt Sum sqr (S-X))^2 < r^2 by A1,A3,SQUARE_1:16;
  then
A13: C < 0 by A12,XREAL_1:49;
  then
A14: C/A < 0 by A10,XREAL_1:141;
  set l2 = (- B + sqrt delta(A,B,C)) / (2 * A);
  set l1 = (- B - sqrt delta(A,B,C)) / (2 * A);
  take e1 = (1-l2)*s+l2*t;
A15: 0 <= --r by A7;
A16: delta(A,B,C) = B^2 - 4*A*C & B^2 >= 0 by QUIN_1:def 1,XREAL_1:63;
A17: for x being Real holds Polynom(A,B,C,x) = Quard(A,l1,l2,x)
  proof
    let x be Real;
    thus Polynom(A,B,C,x) = A*x^2+B*x+C by POLYEQ_1:def 2
      .= A*(x-l1)*(x-l2) by A10,A13,A16,QUIN_1:16
      .= A*((x-l1)*(x-l2))
      .= Quard(A,l1,l2,x) by POLYEQ_1:def 3;
  end;
  then C/A = l1*l2 by A10,POLYEQ_1:11;
  then
A18: l1 < 0 & l2 > 0 or l1 > 0 & l2 < 0 by A14,XREAL_1:133;
A19: A*l2^2+B*l2--C = Polynom(A,B,C,l2) by POLYEQ_1:def 2
    .= Quard(A,l1,l2,l2) by A17
    .= A*((l2-l1)*(l2-l2)) by POLYEQ_1:def 3
    .= 0;
  |. e1 - x .|^2 = |. 1 * s - l2*s + l2*t - x .|^2 by RLVECT_1:35
    .= |. s - l2*s + l2*t - x .|^2 by RLVECT_1:def 8
    .= |. s + l2*t - l2*s - x .|^2 by RLVECT_1:def 3
    .= |. s + (l2*t - l2*s) - x .|^2 by RLVECT_1:def 3
    .= |. s - x + (l2*t - l2*s) .|^2 by RLVECT_1:def 3
    .= |. s-x + l2*(t-s) .|^2 by RLVECT_1:34
    .= |. s-x .|^2 + 2*|(l2*(t-s),s-x)| + |. l2*(t-s) .|^2 by EUCLID_2:45
    .= Sum sqr (S-X) + 2*(l2*|(t-s,s-x)|) + |. l2*(t-s) .|^2
         by A12,A1,A3,EUCLID_2:19
    .= Sum sqr (S-X) + 2*l2*|(t-s,s-x)| + (|.l2.|*|. t-s .|)^2 by TOPRNS_1:7
    .= Sum sqr (S-X) + 2*l2*|(t-s,s-x)| + (|.l2.|)^2*|. t-s .|^2
    .= Sum sqr (S-X) + l2*(2 * |(t-s,s-x)|) + l2^2*(|. T-S .|^2)
            by A1,A2,COMPLEX1:75
    .= Sum sqr (S-X) + l2*B + l2^2*A by A4,SQUARE_1:def 2
    .= r^2 by A19;
  then |. e1 - x .| = r or |. e1 - x .| = -r by SQUARE_1:40;
  then
A20: e1 in Sphere(x,r) by A15,A11;
A21: 4*A*C < 0 by A10,A13,XREAL_1:129,132;
  then
A22: e1 in halfline(s,t) by A10,A16,A18,QUIN_1:25;
  hereby
    let d be object;
    assume d in {e1};
    then d = e1 by TARSKI:def 1;
    hence d in halfline(s,t) /\ Sphere(x,r) by A22,A20,XBOOLE_0:def 4;
  end;
  hereby
    let d be object;
    assume
A23: d in halfline(s,t) /\ Sphere(x,r);
    then d in halfline(s,t) by XBOOLE_0:def 4;
    then consider l being Real such that
A24: d = (1-l)*s+l*t and
A25: 0 <= l;
A26: |. l*(t-s) .|^2 = (|.l.|*|. t-s .|)^2 by TOPRNS_1:7
      .= |.l.|^2 * |. t-s .|^2
      .= l^2 * |. t-s .|^2 by COMPLEX1:75;
    d in Sphere(x,r) by A23,XBOOLE_0:def 4;
    then r = |. (1-l)*s+l*t - x .| by A24,Th7
      .= |. 1 * s - l*s + l*t - x .| by RLVECT_1:35
      .= |. s - l*s + l*t - x .| by RLVECT_1:def 8
      .= |. s - (l*s - l*t) - x .| by RLVECT_1:29
      .= |. s +- (l*s - l*t) +- x .|
      .= |. s +-x +- (l*s - l*t) .| by RLVECT_1:def 3
      .= |. s-x - (l*s - l*t) .|
      .= |. s +-x  +-(l*s - l*t) .|
      .= |. s-x +- l*(s-t) .| by RLVECT_1:34
      .= |. s-x + l*(-(s-t)) .| by RLVECT_1:25
      .= |. s-x + l*(t-s) .| by RLVECT_1:33;
    then r^2 = |. s-x .|^2 + 2*|(l*(t-s),s-x)| + |. l*(t-s) .|^2 by EUCLID_2:45
      .= |. s-x .|^2 + 2*(l*|(t-s,s-x)|) + |. l*(t-s) .|^2 by EUCLID_2:19;
    then A*l^2+B*l+C = 0 by A5,A12,A1,A3,A2,A26;
    then Polynom(A,B,C,l) = 0 by POLYEQ_1:def 2;
    then l = l1 or l = l2 by A10,A13,A16,POLYEQ_1:5;
    hence d in {e1} by A10,A21,A16,A18,A24,A25,QUIN_1:25,TARSKI:def 1;
  end;
  thus thesis by A8;
end;

theorem Th36:
  for S, T, Y being Element of REAL n st S = 1/2*y + 1/2*z & T = z
  & Y = x & y <> z & y in Sphere(x,r) & z in cl_Ball(x,r) ex e being Point of
TOP-REAL n st e <> y & {y,e} = halfline(y,z) /\ Sphere(x,r) & (z in Sphere(x,r)
implies e = z) & (not z in Sphere(x,r) & a = (-(2*|(z-(1/2*y + 1/2*z),1/2*y + 1
/2*z-x)|) + sqrt delta (Sum sqr (T-S), 2 * |(z-(1/2*y + 1/2*z),1/2*y + 1/2*z-x
)|, Sum sqr (S-Y) - r^2)) / (2 * Sum sqr (T-S)) implies e = (1-a)*(1/2*y + 1/2*
  z) + a*z)
proof
  let S, T, Y be Element of REAL n such that
A1: S = 1/2*y + 1/2*z & T = z & Y = x;
  reconsider G = x as Point of Euclid n by TOPREAL3:8;
  set s = y, t = z;
  set X = 1/2 * s + 1/2 * t;
  assume that
A2: s <> t and
A3: s in Sphere(x,r) and
A4: t in cl_Ball(x,r);
A5: Ball(G,r) = Ball(x,r) by Th11;
A6: Sphere(x,r) c= cl_Ball(x,r) by Th15;
  per cases;
  suppose
A7: t in Sphere(x,r);
    take t;
    thus thesis by A2,A3,A7,Th34;
  end;
  suppose
A8: not t in Sphere(x,r);
A9: now
      assume
A10:     X = t;
      t +- 1/2 * s +- 1/2 * t = t - 1/2 * s - 1/2 * t
        .= t - t by A10,RLVECT_1:27
        .= 0.TOP-REAL n by RLVECT_1:5;
      then 0.TOP-REAL n
         = t +- 1/2 * t +- 1/2 * s by RLVECT_1:def 3
        .= 1 * t - 1/2 * t - 1/2 * s by RLVECT_1:def 8
        .= (1-1/2) * t - 1/2 * s by RLVECT_1:35
        .= 1/2 * (t-s) by RLVECT_1:34;
      then t-s = 0.TOP-REAL n by RLVECT_1:11;
      hence contradiction by A2,RLVECT_1:21;
    end;
    Ball(x,r) \/ Sphere(x,r) = cl_Ball(x,r) by Th16;
    then
A11: t in Ball(G,r) by A4,A5,A8,XBOOLE_0:def 3;
    set a = (-(2*|(t-X,X-x)|) + sqrt delta (Sum sqr (T-S), 2 * |(t-X,X-x)|,
    Sum sqr (S-Y) - r^2)) / (2 * Sum sqr (T-S));
A12: 1/2 + 1/2 = 1 & |.1/2.| = 1/2 by ABSVALUE:def 1;
    Ball(G,r) = Ball(x,r) by Th11;
    then X in Ball(G,r) by A3,A6,A12,A11,Th22;
    then consider e1 being Point of TOP-REAL n such that
A13: {e1} = halfline(X,t) /\ Sphere(x,r) and
A14: e1 = (1-a)*X + a*t by A1,A5,A9,Th35;
    take e1;
A15: e1 in {e1} by TARSKI:def 1;
    then e1 in halfline(X,t) by A13,XBOOLE_0:def 4;
    then consider l being Real such that
A16: e1 = (1-l)*X + l*t and
A17: 0 <= l;
    hereby
      assume e1 = s;
      then 0.TOP-REAL n = (1-l)*X + l*t - s by A16,RLVECT_1:5
        .= (1-l)*(1/2*s) + (1-l)*(1/2*t) + l*t - s by RLVECT_1:def 5
        .= (1-l)*(1/2*s) + ((1-l)*(1/2*t) + l*t) - s by RLVECT_1:def 3
        .= (1-l)*(1/2*s) - s + ((1-l)*(1/2*t) + l*t) by RLVECT_1:def 3
        .= (1-l)*(1/2*s) - 1 * s + ((1-l)*(1/2*t) + l*t) by RLVECT_1:def 8
        .= (1-l)*(1/2)*s - 1 * s + ((1-l)*(1/2*t) + l*t) by RLVECT_1:def 7
        .= ((1-l)*(1/2) - 1) * s + ((1-l)*(1/2*t) + l*t) by RLVECT_1:35
        .= (-1/2 - l*(1/2)) * s + ((1-l)*(1/2)*t + l*t) by RLVECT_1:def 7
        .= (-1/2 - l*(1/2)) * s + ((1-l)*(1/2) + l) * t by RLVECT_1:def 6
        .= (-(1/2 + l*(1/2))) * s + (1/2 + l*(1/2)) * t
        .= (1/2 + l*(1/2)) * t - (1/2 + l*(1/2)) * s by RLVECT_1:79
        .= (1/2 + l*(1/2)) * (t - s) by RLVECT_1:34;
      then 1/2 + l*(1/2) = 0 or t - s = 0.TOP-REAL n by RLVECT_1:11;
      hence contradiction by A2,A17,RLVECT_1:21;
    end;
A18: s in halfline(s,t) by Th25;
    hereby
      set o = (1+l)/2;
      let m be object;
      assume m in {s,e1};
      then
A19:  m = s or m = e1 by TARSKI:def 2;
      e1 = (1-l)*(1/2*s) + (1-l)*(1/2*t) + l*t by A16,RLVECT_1:def 5
        .= (1-l)*(1/2)*s + (1-l)*(1/2*t) + l*t by RLVECT_1:def 7
        .= (1-l)*(1/2)*s + (1-l)*(1/2)*t + l*t by RLVECT_1:def 7
        .= (1-l)*(1/2)*s + ((1-l)*(1/2)*t + l*t) by RLVECT_1:def 3
        .= (1-l)*(1/2)*s + ((1-l)*(1/2) + l)*t by RLVECT_1:def 6
        .= (1-o)*s + o*t;
      then
A20:  e1 in halfline(s,t) by A17;
      e1 in Sphere(x,r) by A13,A15,XBOOLE_0:def 4;
      hence m in halfline(s,t) /\ Sphere(x,r) by A3,A18,A19,A20,XBOOLE_0:def 4;
    end;
    hereby
      let m be object;
      assume
A21:  m in halfline(s,t) /\ Sphere(x,r);
      then
A22:  m in halfline(s,t) by XBOOLE_0:def 4;
A23:  m in Sphere(x,r) by A21,XBOOLE_0:def 4;
      per cases;
      suppose
        m in halfline(X,t);
        then m in halfline(X,t) /\ Sphere(x,r) by A23,XBOOLE_0:def 4;
        then m = e1 by A13,TARSKI:def 1;
        hence m in {s,e1} by TARSKI:def 2;
      end;
      suppose
A24:    not m in halfline(X,t);
        consider M being Real such that
A25:    m = (1-M)*s + M*t and
A26:    0 <= M by A22;
A27:    now
          set o = 2*M-1;
          assume M > 1;
          then 2*M > 2*1 by XREAL_1:68;
          then
A28:      2*M-1 > 2*1-1 by XREAL_1:14;
          (1-o)*X + o*t = (1-o)*(1/2 * s) + (1-o)*(1/2 * t) + o*t by
RLVECT_1:def 5
            .= (1-o)*(1/2) * s + (1-o)*(1/2 * t) + o*t by RLVECT_1:def 7
            .= (1-o)*(1/2) * s + (1-o)*(1/2) * t + o*t by RLVECT_1:def 7
            .= (1-o)*(1/2) * s + ((1-o)*(1/2) * t + o*t) by RLVECT_1:def 3
            .= (1-o)*(1/2) * s + ((1-o)*(1/2)+o) * t by RLVECT_1:def 6
            .= m by A25;
          hence contradiction by A24,A28;
        end;
        |. t-x .| <= r & |. t-x .| <> r by A4,A8,Th6;
        then |. t-x .| < r by XXREAL_0:1;
        then t in Ball(x,r);
        then
A29:    LSeg(s,t) /\ Sphere(x,r) = {s} by A3,Th31;
        m in LSeg(s,t) by A25,A26,A27;
        then m in {s} by A23,A29,XBOOLE_0:def 4;
        then m = s by TARSKI:def 1;
        hence m in {s,e1} by TARSKI:def 2;
      end;
    end;
    thus thesis by A8,A14;
  end;
end;

registration
  let n be Nat, x be Point of TOP-REAL n;
  let r be negative Real;
  cluster Sphere(x,r) -> empty;
  coherence
  proof
    assume not thesis;
    then consider y being Point of TOP-REAL n such that
A1: y in Sphere(x,r);
    |. y - x .| = r by A1,Th7;
    hence contradiction;
  end;
end;

registration
  let n be non zero Nat, x be Point of TOP-REAL n;
  let r be non negative Real;
  cluster Sphere(x,r) -> non empty;
  coherence
  proof
    reconsider e = x as Point of Euclid n by TOPREAL3:8;
    per cases;
    suppose
      r = 0;
      then Sphere(e,r) = {e} by TOPREAL6:54;
      hence thesis by Th13;
    end;
    suppose
      r > 0;
      then reconsider r as positive Real;
      consider s being Point of TOP-REAL n such that
A1:   s in Ball(x,r) by SUBSET_1:4;
      reconsider S = s, T = s + 1.REAL n, XX = x as Element of REAL n by
EUCLID:22;
      set a = (-(2*|(s + 1.REAL n-s,s-x)|) + sqrt delta (Sum sqr (T-S), 2 * |(
      s + 1.REAL n-s,s-x)|, Sum sqr (S-XX) - r^2)) / (2 * Sum sqr (T-S));
      s <> s + 1.REAL n by Th1;
      then
      ex e being Point of TOP-REAL n st {e} = halfline(s,s + 1.REAL n) /\
      Sphere(x,r) & e = (1-a)*s + a*(s+1.REAL n) by A1,Th35;
      hence thesis;
    end;
  end;
end;

theorem
  Sphere(x,r) is non empty implies r >= 0;

theorem
  n is non zero & Sphere(x,r) is empty implies r < 0;

begin :: Subsets of TOP-REAL 2

reserve s, t for Point of TOP-REAL 2;

theorem
  (a*s + b*t)`1 = a * s`1 + b * t`1
proof
  thus (a*s+b*t)`1 = (a*s)`1 + (b*t)`1 by TOPREAL3:2
    .= a*s`1 + (b*t)`1 by TOPREAL3:4
    .= a*s`1+b*t`1 by TOPREAL3:4;
end;

theorem
  (a*s + b*t)`2 = a * s`2 + b * t`2
proof
  thus (a*s+b*t)`2 = (a*s)`2 + (b*t)`2 by TOPREAL3:2
    .= a*s`2 + (b*t)`2 by TOPREAL3:4
    .= a*s`2+b*t`2 by TOPREAL3:4;
end;

theorem Th41:
  t in circle(a,b,r) iff |. t - |[a,b]| .| = r
proof
A1: circle(a,b,r) = {x where x is Point of TOP-REAL 2: |. x - |[a,b]| .| = r
  } by JGRAPH_6:def 5;
  hereby
    assume t in circle(a,b,r);
    then
    ex x being Point of TOP-REAL 2 st t = x & |. x - |[a,b]| .| = r by A1;
    hence |. t - |[a,b]| .| = r;
  end;
  thus thesis by A1;
end;

theorem Th42:
  t in closed_inside_of_circle(a,b,r) iff |. t - |[a,b]| .| <= r
proof
A1: closed_inside_of_circle(a,b,r) = {x where x is Point of TOP-REAL 2: |. x
  - |[a,b]| .| <= r} by JGRAPH_6:def 7;
  hereby
    assume t in closed_inside_of_circle(a,b,r);
    then
    ex x being Point of TOP-REAL 2 st t = x & |. x - |[a,b]| .| <= r by A1;
    hence |. t - |[a,b]| .| <= r;
  end;
  thus thesis by A1;
end;

theorem Th43:
  t in inside_of_circle(a,b,r) iff |. t - |[a,b]| .| < r
proof
A1: inside_of_circle(a,b,r) = {x where x is Point of TOP-REAL 2: |. x - |[a,
  b]| .| < r} by JGRAPH_6:def 6;
  hereby
    assume t in inside_of_circle(a,b,r);
    then
    ex x being Point of TOP-REAL 2 st t = x & |. x - |[a,b]| .| < r by A1;
    hence |. t - |[a,b]| .| < r;
  end;
  thus thesis by A1;
end;

registration
  let a, b be Real;
  let r be positive Real;
  cluster inside_of_circle(a,b,r) -> non empty;
  coherence
  proof
    |. |[a,b]| - |[a,b]| .| = 0 by TOPRNS_1:28;
    hence thesis by Th43;
  end;
end;

registration
  let a, b be Real;
  let r be non negative Real;
  cluster closed_inside_of_circle(a,b,r) -> non empty;
  coherence
  proof
    |. |[a,b]| - |[a,b]| .| = 0 by TOPRNS_1:28;
    hence thesis by Th42;
  end;
end;

theorem
  circle(a,b,r) c= closed_inside_of_circle(a,b,r)
proof
  let x be object;
  assume
A1: x in circle(a,b,r);
  then reconsider x as Point of TOP-REAL 2;
  |. x - |[a,b]| .| = r by A1,Th41;
  hence thesis by Th42;
end;

theorem Th45:
  for x being Point of Euclid 2 st x = |[a,b]| holds cl_Ball(x,r)
  = closed_inside_of_circle(a,b,r)
proof
  let x be Point of Euclid 2 such that
A1: x = |[a,b]|;
  hereby
    let w be object;
    assume
A2: w in cl_Ball(x,r);
    then reconsider u = w as Point of TOP-REAL 2 by TOPREAL3:8;
    reconsider e = u as Point of Euclid 2 by TOPREAL3:8;
    dist(e,x) = |. u - |[a,b]| .| by A1,JGRAPH_1:28;
    then |. u - |[a,b]| .| <= r by A2,METRIC_1:12;
    hence w in closed_inside_of_circle(a,b,r) by Th42;
  end;
  let w be object;
  assume
A3: w in closed_inside_of_circle(a,b,r);
  then reconsider u = w as Point of TOP-REAL 2;
  reconsider e = u as Point of Euclid 2 by TOPREAL3:8;
  dist(e,x) = |. u - |[a,b]| .| by A1,JGRAPH_1:28;
  then dist(e,x) <= r by A3,Th42;
  hence thesis by METRIC_1:12;
end;

theorem Th46:
  for x being Point of Euclid 2 st x = |[a,b]| holds Ball(x,r) =
  inside_of_circle(a,b,r)
proof
  let x be Point of Euclid 2 such that
A1: x = |[a,b]|;
  hereby
    let w be object;
    assume
A2: w in Ball(x,r);
    then reconsider u = w as Point of TOP-REAL 2 by TOPREAL3:8;
    reconsider e = u as Point of Euclid 2 by TOPREAL3:8;
    dist(e,x) = |. u - |[a,b]| .| by A1,JGRAPH_1:28;
    then |. u - |[a,b]| .| < r by A2,METRIC_1:11;
    hence w in inside_of_circle(a,b,r) by Th43;
  end;
  let w be object;
  assume
A3: w in inside_of_circle(a,b,r);
  then reconsider u = w as Point of TOP-REAL 2;
  reconsider e = u as Point of Euclid 2 by TOPREAL3:8;
  dist(e,x) = |. u - |[a,b]| .| by A1,JGRAPH_1:28;
  then dist(e,x) < r by A3,Th43;
  hence thesis by METRIC_1:11;
end;

theorem Th47:
  for x being Point of Euclid 2 st x = |[a,b]| holds Sphere(x,r) =
  circle(a,b,r)
proof
  let x be Point of Euclid 2 such that
A1: x = |[a,b]|;
  hereby
    let w be object;
    assume
A2: w in Sphere(x,r);
    then reconsider u = w as Point of TOP-REAL 2 by TOPREAL3:8;
    reconsider e = u as Point of Euclid 2 by TOPREAL3:8;
    dist(e,x) = |. u - |[a,b]| .| by A1,JGRAPH_1:28;
    then |. u - |[a,b]| .| = r by A2,METRIC_1:13;
    hence w in circle(a,b,r) by Th41;
  end;
  let w be object;
  assume
A3: w in circle(a,b,r);
  then reconsider u = w as Point of TOP-REAL 2;
  reconsider e = u as Point of Euclid 2 by TOPREAL3:8;
  dist(e,x) = |. u - |[a,b]| .| by A1,JGRAPH_1:28;
  then dist(e,x) = r by A3,Th41;
  hence thesis by METRIC_1:13;
end;

theorem Th48:
  Ball(|[a,b]|,r) = inside_of_circle(a,b,r)
proof
  reconsider e = |[a,b]| as Point of Euclid 2 by TOPREAL3:8;
  thus Ball(|[a,b]|,r) = Ball(e,r) by Th11
    .= inside_of_circle(a,b,r) by Th46;
end;

theorem
  cl_Ball(|[a,b]|,r) = closed_inside_of_circle(a,b,r)
proof
  reconsider e = |[a,b]| as Point of Euclid 2 by TOPREAL3:8;
  thus cl_Ball(|[a,b]|,r) = cl_Ball(e,r) by Th12
    .= closed_inside_of_circle(a,b,r) by Th45;
end;

theorem Th50:
  Sphere(|[a,b]|,r) = circle(a,b,r)
proof
  reconsider e = |[a,b]| as Point of Euclid 2 by TOPREAL3:8;
  thus Sphere(|[a,b]|,r) = Sphere(e,r) by Th13
    .= circle(a,b,r) by Th47;
end;

theorem
  inside_of_circle(a,b,r) c= closed_inside_of_circle(a,b,r)
proof
  let x be object;
  assume
A1: x in inside_of_circle(a,b,r);
  then reconsider x as Point of TOP-REAL 2;
  |. x - |[a,b]| .| < r by A1,Th43;
  hence thesis by Th42;
end;

theorem
  inside_of_circle(a,b,r) misses circle(a,b,r)
proof
  assume not thesis;
  then consider x being object such that
A1: x in inside_of_circle(a,b,r) and
A2: x in circle(a,b,r) by XBOOLE_0:3;
  reconsider x as Point of TOP-REAL 2 by A1;
  |. x - |[a,b]| .| = r by A2,Th41;
  hence thesis by A1,Th43;
end;

theorem
  inside_of_circle(a,b,r) \/ circle(a,b,r) = closed_inside_of_circle(a,b ,r)
proof
  reconsider p = |[a,b]| as Point of Euclid 2 by TOPREAL3:8;
A1: cl_Ball(p,r) = closed_inside_of_circle(a,b,r) by Th45;
  Sphere(p,r) = circle(a,b,r) & Ball(p,r) = inside_of_circle(a,b,r) by Th46
,Th47;
  hence thesis by A1,METRIC_1:16;
end;

theorem
  s in Sphere(0.TOP-REAL 2,r) implies s`1^2 + s`2^2 = r^2
proof
  assume s in Sphere(0.TOP-REAL 2,r);
  then |. s-0.TOP-REAL 2 .| = r by Th7;
  then |. s .| = r by RLVECT_1:13;
  hence thesis by JGRAPH_1:29;
end;

theorem
  s <> t & s in closed_inside_of_circle(a,b,r) & t in
  closed_inside_of_circle(a,b,r) implies r > 0
proof
  reconsider x = |[a,b]| as Point of Euclid 2 by TOPREAL3:8;
  cl_Ball(x,r) = closed_inside_of_circle(a,b,r) by Th45;
  hence thesis by Th4;
end;

theorem
  for S, T, X being Element of REAL 2 st S = s & T = t & X = |[a,b]| & w
  = (-(2*|(t-s,s-|[a,b]|)|) + sqrt delta (Sum sqr (T-S), 2 * |(t-s,s-|[a,b]|)|,
Sum sqr (S-X) - r^2)) / (2 * Sum sqr (T-S)) & s <> t & s in inside_of_circle(a,
b,r) ex e being Point of TOP-REAL 2 st {e} = halfline(s,t) /\ circle(a,b,r) & e
  = (1-w)*s + w*t
proof
A1: Ball(|[a,b]|,r) = inside_of_circle(a,b,r) & Sphere(|[a,b]|,r) = circle(a
  ,b,r ) by Th48,Th50;
  let S, T, X be Element of REAL 2;
  assume S = s & T = t & X = |[a,b]| & w = (-(2*|(t-s,s-|[a,b]|)|) + sqrt
delta ( Sum sqr (T-S), 2 * |(t-s,s-|[a,b]|)|, Sum sqr (S-X) - r^2)) / (2 * Sum
  sqr (T-S )) & s <> t & s in inside_of_circle(a,b,r);
  hence thesis by A1,Th35;
end;

theorem
  s in circle(a,b,r) & t in inside_of_circle(a,b,r) implies LSeg(s,t) /\
  circle(a,b,r) = {s}
proof
  assume
A1: s in circle(a,b,r) & t in inside_of_circle(a,b,r);
  reconsider e = |[a,b]| as Point of Euclid 2 by TOPREAL3:8;
A2: inside_of_circle(a,b,r) = Ball(e,r) by Th46
    .= Ball(|[a,b]|,r) by Th11;
  circle(a,b,r) = Sphere(e,r) by Th47
    .= Sphere(|[a,b]|,r) by Th13;
  hence thesis by A1,A2,Th31;
end;

theorem
  s in circle(a,b,r) & t in circle(a,b,r) implies LSeg(s,t) \ {s,t} c=
  inside_of_circle(a,b,r)
proof
  assume
A1: s in circle(a,b,r) & t in circle(a,b,r);
  reconsider G = |[a,b]| as Point of Euclid 2 by TOPREAL3:8;
  Sphere(G,r) = circle(a,b,r) by Th47;
  then
A2: Sphere(|[a,b]|,r) = circle(a,b,r) by Th13;
  Ball(|[a,b]|,r) = inside_of_circle(a,b,r) by Th48;
  hence thesis by A1,A2,Th32;
end;

theorem
  s in circle(a,b,r) & t in circle(a,b,r) implies LSeg(s,t) /\ circle(a,
  b,r) = {s,t}
proof
  reconsider G = |[a,b]| as Point of Euclid 2 by TOPREAL3:8;
  Sphere(G,r) = circle(a,b,r) by Th47;
  then
A1: Sphere(|[a,b]|,r) = circle(a,b,r) by Th13;
  assume s in circle(a,b,r) & t in circle(a,b,r);
  hence thesis by A1,Th33;
end;

theorem
  s in circle(a,b,r) & t in circle(a,b,r) implies halfline(s,t) /\
  circle(a,b,r) = {s,t}
proof
  assume
A1: s in circle(a,b,r) & t in circle(a,b,r);
  reconsider e = |[a,b]| as Point of Euclid 2 by TOPREAL3:8;
  circle(a,b,r) = Sphere(e,r) by Th47
    .= Sphere(|[a,b]|,r) by Th13;
  hence thesis by A1,Th34;
end;

theorem
  for S, T, Y being Element of REAL 2 st S = 1/2*s + 1/2*t & T = t & Y =
|[a,b]| & s <> t & s in circle(a,b,r) & t in closed_inside_of_circle(a,b,r) ex
e being Point of TOP-REAL 2 st e <> s & {s,e} = halfline(s,t) /\ circle(a,b,r)
& (t in Sphere(|[a,b]|,r) implies e = t) & (not t in Sphere(|[a,b]|,r) & w = (-
(2*|(t-(1/2*s + 1/2*t),1/2*s + 1/2*t-|[a,b]|)|) + sqrt delta (Sum sqr (T-S), 2
* |(t-(1/2*s + 1/2*t),1/2*s + 1/2*t-|[a,b]|)|, Sum sqr (S-Y) - r^2)) / (2 * Sum
  sqr (T-S)) implies e = (1-w)*(1/2*s + 1/2*t) + w*t)
proof
  reconsider G = |[a,b]| as Point of Euclid 2 by TOPREAL3:8;
A1: cl_Ball(G,r) = closed_inside_of_circle(a,b,r) & cl_Ball(G,r) = cl_Ball(
  |[a,b ]|,r) by Th12,Th45;
  Sphere(G,r) = circle(a,b,r) by Th47;
  then
A2: Sphere(|[a,b]|,r) = circle(a,b,r) by Th13;
  let S, T, Y be Element of REAL 2;
  assume S = 1/2*s + 1/2*t & T = t & Y = |[a,b]| & s <> t & s in circle(a,b,r
  ) & t in closed_inside_of_circle(a,b,r);
  hence thesis by A1,A2,Th36;
end;

registration
  let a, b, r be Real;
  cluster inside_of_circle(a,b,r) -> convex;
  coherence
  proof
    inside_of_circle(a,b,r) = {q where q is Point of TOP-REAL 2: |.q - |[a
    ,b]|.| < r } by JGRAPH_6:def 6;
    hence thesis by Lm2;
  end;
  cluster closed_inside_of_circle(a,b,r) -> convex;
  coherence
  proof
    closed_inside_of_circle(a,b,r) = {q where q is Point of TOP-REAL 2: |.
    q - |[a,b]|.| <= r } by JGRAPH_6:def 7;
    hence thesis by Lm1;
  end;
end;

:: 12.11.18 A.T.

theorem Th62:
 for V being RealLinearSpace, p1,p2 being Point of V
  holds halfline(p1,p2) c= Line(p1,p2)
proof
 let V be RealLinearSpace, p1,p2 be Point of V;
 let e be object;
 assume e in halfline(p1,p2);
  then ex r st e =(1-r)*p1 + r*p2 & 0 <= r;
 hence e in Line(p1,p2);
end;

theorem Th63:
 for V being RealLinearSpace, p1,p2 being Point of V
  holds Line(p1,p2) = halfline(p1,p2) \/ halfline(p2,p1)
proof
 let V be RealLinearSpace, p1,p2 be Point of V;
 thus Line(p1,p2) c= halfline(p1,p2) \/ halfline(p2,p1)
  proof let e be object;
   assume e in Line(p1,p2);
    then consider r such that
A1:   e = (1-r)*p1 + r*p2;
    now per cases;
     case r >= 0;
      hence e in halfline(p1,p2) by A1;
     end;
     case r <= 0;
      then
A2:     1-r >= 0;
       e = (1-(1-r))*p2 + (1-r)*p1 by A1;
      hence e in halfline(p2,p1) by A2;
     end;
    end;
   hence thesis by XBOOLE_0:def 3;
  end;
  halfline(p1,p2) c= Line(p1,p2) & halfline(p2,p1) c= Line(p1,p2) by Th62;
 hence thesis by XBOOLE_1:8;
end;

theorem Th64:
 for V being RealLinearSpace, p1,p2,p3 being Point of V
   st p1 in halfline(p2,p3)
  holds p1 in LSeg(p2,p3) or p3 in LSeg(p2,p1)
proof let V be RealLinearSpace, p1,p2,p3 be Point of V;
 assume p1 in halfline(p2,p3);
  then consider r such that
A1: p1 = (1-r)*p2 + r*p3 and
A2: 0 <= r;
  set s = 1/r;
  now per cases;
   case r <= 1;
    hence p1 in LSeg(p2,p3) by A1,A2;
   end;
   case
A3:  r >= 1;
    per cases by A2;
    case r = 0;
      then p1 = p2 by A1,Th2;
     hence p1 in LSeg(p2,p3) by RLTOPSP1:68;
    end;
    case
A4:  r > 0;
     then
A5:  s*r = 1 by XCMPLX_1:87;
A6:  s <= 1 by A3,XREAL_1:183;
A7:  r*p3 = p1 - (1-r)*p2 by RLVECT_4:1,A1;
    (s*r)*p3 = s*(r*p3) by RLVECT_1:def 7
           .= s*p1 - s*((1-r)*p2) by RLVECT_1:34,A7
           .= s*p1 - s*(1-r)*p2 by RLVECT_1:def 7;
    then p3 = s*p1 - s*(1-r)*p2 by RLVECT_1:def 8,A5
           .= s*p1 + (-s*(1-r))*p2 by RLVECT_1:79
           .= s*p1 + (1-s)*p2 by A5;
    hence p3 in LSeg(p2,p1) by A4,A6;
    end;
   end;
  end;
 hence thesis;
end;

theorem
 for V being RealLinearSpace, p1,p2,p3 being Point of V holds
  p1,p2,p3 are_collinear iff
   p1 in LSeg(p2,p3) or p2 in LSeg(p3, p1) or p3 in LSeg(p1,p2)
proof let V be RealLinearSpace, p1,p2,p3 be Point of V;
 thus p1,p2,p3 are_collinear implies
   p1 in LSeg(p2,p3) or p2 in LSeg(p3, p1) or p3 in LSeg(p1,p2)
 proof assume p1,p2,p3 are_collinear;
   then consider L being line of V such that
A1: p1 in L and
A2: p2 in L and
A3: p3 in L;
  consider x1,x2 being Point of V such that
A4: L = Line(x1,x2) by RLTOPSP1:def 15;
  per cases;
  suppose p2 = p3;
   hence thesis by RLTOPSP1:68;
  end;
  suppose p2 <> p3;
   then
A5: Line(p2,p3) = L by A2,A3,RLTOPSP1:75,A4;
  per cases;
  suppose p1 in halfline(p2,p3);
  hence thesis by Th64;
  end;
  suppose
A6:  not p1 in halfline(p2,p3);
   L = halfline(p2,p3) \/ halfline(p3,p2) by Th63,A5;
   then p1 in halfline(p3,p2) by A1,XBOOLE_0:def 3,A6;
  hence thesis by Th64;
  end;
 end;
 end;
 assume p1 in LSeg(p2,p3) or p2 in LSeg(p3, p1) or p3 in LSeg(p1,p2);
  then per cases;
  suppose
A7:  p1 in LSeg(p2,p3);
   take Line(p2,p3);
    LSeg(p2,p3) c= Line(p2,p3) by RLTOPSP1:73;
   hence p1 in Line(p2,p3) by A7;
   thus p2 in Line(p2,p3) by RLTOPSP1:72;
   thus p3 in Line(p2,p3) by RLTOPSP1:72;
  end;
  suppose
A8:  p2 in LSeg(p3, p1);
   take Line(p3,p1);
   thus p1 in Line(p3,p1) by RLTOPSP1:72;
    LSeg(p3,p1) c= Line(p3,p1) by RLTOPSP1:73;
   hence p2 in Line(p3,p1) by A8;
   thus p3 in Line(p3,p1) by RLTOPSP1:72;
  end;
  suppose
A9:  p3 in LSeg(p1,p2);
   take Line(p1,p2);
   thus p1 in Line(p1,p2) by RLTOPSP1:72;
   thus p2 in Line(p1,p2) by RLTOPSP1:72;
    LSeg(p1,p2) c= Line(p1,p2) by RLTOPSP1:73;
   hence p3 in Line(p1,p2) by A9;
  end;
end;