topreal9.miz



    begin

    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);

    ::$Canceled

    theorem :: TOPREAL9:3

    

     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 :: TOPREAL9:4

    

     Th2: for V be RealLinearSpace, y,z be Point of V holds for x be 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 :: TOPREAL9:5

    

     Th3: for f be 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 :: TOPREAL9:6

    

     Th4: for M be non empty MetrSpace, z1,z2,z3 be 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

    definition

      let n be Nat, x be Point of ( TOP-REAL n), r be Real;

      :: TOPREAL9:def1

      func Ball (x,r) -> Subset of ( TOP-REAL n) equals { p where p be Point of ( TOP-REAL n) : |.(p - x).| < r };

      coherence

      proof

        { p where p be 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 be Point of ( TOP-REAL n) : |.(p - x).| < r };

          then ex p be Point of ( TOP-REAL n) st q = p & |.(p - x).| < r;

          hence thesis;

        end;

        hence thesis;

      end;

      :: TOPREAL9:def2

      func cl_Ball (x,r) -> Subset of ( TOP-REAL n) equals { p where p be Point of ( TOP-REAL n) : |.(p - x).| <= r };

      coherence

      proof

        { p where p be 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 be Point of ( TOP-REAL n) : |.(p - x).| <= r };

          then ex p be Point of ( TOP-REAL n) st q = p & |.(p - x).| <= r;

          hence thesis;

        end;

        hence thesis;

      end;

      :: TOPREAL9:def3

      func Sphere (x,r) -> Subset of ( TOP-REAL n) equals { p where p be Point of ( TOP-REAL n) : |.(p - x).| = r };

      coherence

      proof

        { p where p be 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 be Point of ( TOP-REAL n) : |.(p - x).| = r };

          then ex p be Point of ( TOP-REAL n) st q = p & |.(p - x).| = r;

          hence thesis;

        end;

        hence thesis;

      end;

    end

    theorem :: TOPREAL9:7

    

     Th5: y in ( Ball (x,r)) iff |.(y - x).| < r

    proof

      hereby

        assume y in ( Ball (x,r));

        then ex p be Point of ( TOP-REAL n) st y = p & |.(p - x).| < r;

        hence |.(y - x).| < r;

      end;

      thus thesis;

    end;

    theorem :: TOPREAL9:8

    

     Th6: y in ( cl_Ball (x,r)) iff |.(y - x).| <= r

    proof

      hereby

        assume y in ( cl_Ball (x,r));

        then ex p be Point of ( TOP-REAL n) st y = p & |.(p - x).| <= r;

        hence |.(y - x).| <= r;

      end;

      thus thesis;

    end;

    theorem :: TOPREAL9:9

    

     Th7: y in ( Sphere (x,r)) iff |.(y - x).| = r

    proof

      hereby

        assume y in ( Sphere (x,r));

        then ex p be Point of ( TOP-REAL n) st y = p & |.(p - x).| = r;

        hence |.(y - x).| = r;

      end;

      thus thesis;

    end;

    theorem :: TOPREAL9:10

    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 :: TOPREAL9:11

    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 :: TOPREAL9:12

    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 :: TOPREAL9:13

    

     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 :: TOPREAL9:14

    

     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 :: TOPREAL9:15

    

     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 :: TOPREAL9:16

    ( 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 :: TOPREAL9:17

    

     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 :: TOPREAL9:18

    

     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 :: TOPREAL9:19

    

     Th17: ( Ball (x,r)) misses ( Sphere (x,r))

    proof

      assume not thesis;

      then

      consider q be 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 be 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 :: TOPREAL9:20

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

    theorem :: TOPREAL9:21

    ( 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 be 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 :: TOPREAL9:22

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

    theorem :: TOPREAL9:23

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

    theorem :: TOPREAL9:24

    

     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 be Real, P be Subset of ( TOP-REAL n), Q be Point of ( TOP-REAL n) st P = { q where q be 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 be 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 be Point of ( TOP-REAL n) st q1 = p1 & |.(q1 - Q).| <= a by A1;

      assume

       A3: p2 in P;

      then

       A4: ex q2 be 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 be 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 be Real, P be Subset of ( TOP-REAL n), Q be Point of ( TOP-REAL n) st P = { q where q be 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 be 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;

    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);

      :: TOPREAL9:def4

      attr f is homogeneous means

      : Def4: for r be Real, x be 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 :: TOPREAL9:25

    for f be homogeneous additive Function of ( TOP-REAL n), ( TOP-REAL n), X be 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 be 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 be 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 be 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;

    reserve V for RealLinearSpace,

p,q,x for Element of V;

    definition

      let V, p, q;

      :: TOPREAL9:def5

      func halfline (p,q) -> Subset of V equals { (((1 - l) * p) + (l * q)) where l be Real : 0 <= l };

      coherence

      proof

        set X = { (((1 - l) * p) + (l * q)) where l be Real : 0 <= l };

        X c= the carrier of V

        proof

          let x be object;

          assume x in X;

          then ex l be Real st x = (((1 - l) * p) + (l * q)) & 0 <= l;

          hence thesis;

        end;

        hence thesis;

      end;

    end

    theorem :: TOPREAL9:26

    for x be set holds x in ( halfline (p,q)) iff ex l be 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 :: TOPREAL9:27

    

     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 :: TOPREAL9:28

    

     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 :: TOPREAL9:29

    

     Th27: ( halfline (p,p)) = {p}

    proof

      hereby

        let d be object;

        assume d in ( halfline (p,p));

        then ex r be 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 :: TOPREAL9:30

    

     Th28: x in ( halfline (p,q)) implies ( halfline (p,x)) c= ( halfline (p,q))

    proof

      assume x in ( halfline (p,q));

      then

      consider R be 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 be 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 :: TOPREAL9:31

    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 be 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 be 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 :: TOPREAL9:32

    ( LSeg (p,q)) c= ( halfline (p,q))

    proof

      let a be object;

      assume a in ( LSeg (p,q));

      then ex r be 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 be Real such that

         A1: u = (((1 - a) * p) + (a * q)) and

         A2: 0 <= a;

        assume v in P;

        then

        consider b be 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 be 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 :: TOPREAL9:33

    

     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 be 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 :: TOPREAL9:34

    

     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 be 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 :: TOPREAL9:35

    

     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 :: TOPREAL9:36

    

     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 be 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 be 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 :: TOPREAL9:37

    

     Th35: for S,T,X be 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 be 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 be 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, XREAL_1: 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 be 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 :: TOPREAL9:38

    

     Th36: for S,T,Y be 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)) holds ex e be 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 be 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 be 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 be 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 be 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 be 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 be 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 :: TOPREAL9:39

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

    theorem :: TOPREAL9:40

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

    begin

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

    theorem :: TOPREAL9:41

    (((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 :: TOPREAL9:42

    (((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 :: TOPREAL9:43

    

     Th41: t in ( circle (a,b,r)) iff |.(t - |[a, b]|).| = r

    proof

      

       A1: ( circle (a,b,r)) = { x where x be 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 be 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 :: TOPREAL9:44

    

     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 be 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 be 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 :: TOPREAL9:45

    

     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 be 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 be 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 :: TOPREAL9:46

    ( 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 :: TOPREAL9:47

    

     Th45: for x be 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 :: TOPREAL9:48

    

     Th46: for x be 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 :: TOPREAL9:49

    

     Th47: for x be 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 :: TOPREAL9:50

    

     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 :: TOPREAL9:51

    ( 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 :: TOPREAL9:52

    

     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 :: TOPREAL9:53

    ( 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 :: TOPREAL9:54

    ( inside_of_circle (a,b,r)) misses ( circle (a,b,r))

    proof

      assume not thesis;

      then

      consider x be 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 :: TOPREAL9:55

    (( 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 :: TOPREAL9:56

    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 :: TOPREAL9:57

    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 :: TOPREAL9:58

    for S,T,X be 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)) holds ex e be 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 :: TOPREAL9:59

    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 :: TOPREAL9:60

    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 :: TOPREAL9:61

    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 :: TOPREAL9:62

    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 :: TOPREAL9:63

    for S,T,Y be 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)) holds ex e be 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 be 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 be Point of ( TOP-REAL 2) : |.(q - |[a, b]|).| <= r } by JGRAPH_6:def 7;

        hence thesis by Lm1;

      end;

    end

    theorem :: TOPREAL9:64

    

     Th62: for V be RealLinearSpace, p1,p2 be 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 :: TOPREAL9:65

    

     Th63: for V be RealLinearSpace, p1,p2 be 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 :: TOPREAL9:66

    

     Th64: for V be RealLinearSpace, p1,p2,p3 be 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 :: TOPREAL9:67

    for V be RealLinearSpace, p1,p2,p3 be 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 be line of V such that

         A1: p1 in L and

         A2: p2 in L and

         A3: p3 in L;

        consider x1,x2 be 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));

      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;