topreal3.miz



    begin

    reserve p,p1,p2,p3,p11,p22,q,q1,q2 for Point of ( TOP-REAL 2),

f,h for FinSequence of ( TOP-REAL 2),

r,r1,r2,s,s1,s2 for Real,

u,u1,u2,u5 for Point of ( Euclid 2),

n,m,i,j,k for Nat,

N for Nat,

x,y,z for set;

    begin

    ::$Canceled

    

     Th1: for x,y,z be object holds 1 in ( dom <*x, y, z*>) & 2 in ( dom <*x, y, z*>) & 3 in ( dom <*x, y, z*>) by FINSEQ_1: 81;

    theorem :: TOPREAL3:2

    

     Th2: ((p1 + p2) `1 ) = ((p1 `1 ) + (p2 `1 )) & ((p1 + p2) `2 ) = ((p1 `2 ) + (p2 `2 ))

    proof

      (p1 + p2) = |[((p1 `1 ) + (p2 `1 )), ((p1 `2 ) + (p2 `2 ))]| by EUCLID: 55;

      hence thesis by EUCLID: 52;

    end;

    theorem :: TOPREAL3:3

    ((p1 - p2) `1 ) = ((p1 `1 ) - (p2 `1 )) & ((p1 - p2) `2 ) = ((p1 `2 ) - (p2 `2 ))

    proof

      (p1 - p2) = |[((p1 `1 ) - (p2 `1 )), ((p1 `2 ) - (p2 `2 ))]| by EUCLID: 61;

      hence thesis by EUCLID: 52;

    end;

    theorem :: TOPREAL3:4

    

     Th4: ((r * p) `1 ) = (r * (p `1 )) & ((r * p) `2 ) = (r * (p `2 ))

    proof

      (r * p) = |[(r * (p `1 )), (r * (p `2 ))]| by EUCLID: 57;

      hence thesis by EUCLID: 52;

    end;

    theorem :: TOPREAL3:5

    

     Th5: p1 = <*r1, s1*> & p2 = <*r2, s2*> implies (p1 + p2) = <*(r1 + r2), (s1 + s2)*> & (p1 - p2) = <*(r1 - r2), (s1 - s2)*>

    proof

      

       A1: ( |[r1, s1]| `1 ) = r1 & ( |[r1, s1]| `2 ) = s1 by EUCLID: 52;

      

       A2: ( |[r2, s2]| `1 ) = r2 & ( |[r2, s2]| `2 ) = s2 by EUCLID: 52;

      assume p1 = <*r1, s1*> & p2 = <*r2, s2*>;

      hence thesis by A1, A2, EUCLID: 55, EUCLID: 61;

    end;

    theorem :: TOPREAL3:6

    

     Th6: (p `1 ) = (q `1 ) & (p `2 ) = (q `2 ) implies p = q

    proof

      assume (p `1 ) = (q `1 ) & (p `2 ) = (q `2 );

      

      hence p = |[(q `1 ), (q `2 )]| by EUCLID: 53

      .= q by EUCLID: 53;

    end;

    theorem :: TOPREAL3:7

    

     Th7: u1 = p1 & u2 = p2 implies (( Pitag_dist 2) . (u1,u2)) = ( sqrt ((((p1 `1 ) - (p2 `1 )) ^2 ) + (((p1 `2 ) - (p2 `2 )) ^2 )))

    proof

      assume that

       A1: u1 = p1 and

       A2: u2 = p2;

      reconsider v1 = u1, v2 = u2 as Element of ( REAL 2);

      reconsider p11 = (p1 `1 ), p21 = (p2 `1 ), p12 = (p1 `2 ), p22 = (p2 `2 ) as Element of REAL by XREAL_0:def 1;

      p1 = |[(p1 `1 ), (p1 `2 )]| & u2 = <*(p2 `1 ), (p2 `2 )*> by A2, EUCLID: 53;

      

      then (v1 - v2) = <*( diffreal . (p11,p21)), ( diffreal . (p12,p22))*> by A1, FINSEQ_2: 75

      .= <*((p1 `1 ) - (p2 `1 )), ( diffreal . ((p1 `2 ),(p2 `2 )))*> by BINOP_2:def 10

      .= <*((p1 `1 ) - (p2 `1 )), ((p1 `2 ) - (p2 `2 ))*> by BINOP_2:def 10;

      

      then ( abs (v1 - v2)) = <*( absreal . ((p1 `1 ) - (p2 `1 ))), ( absreal . ((p1 `2 ) - (p2 `2 )))*> by FINSEQ_2: 36

      .= <* |.((p1 `1 ) - (p2 `1 )).|, ( absreal . ((p1 `2 ) - (p2 `2 )))*> by EUCLID:def 2

      .= <* |.((p1 `1 ) - (p2 `1 )).|, |.((p1 `2 ) - (p2 `2 )).|*> by EUCLID:def 2;

      

      then

       A3: ( sqr ( abs (v1 - v2))) = <*( sqrreal . |.((p1 `1 ) - (p2 `1 )).|), ( sqrreal . |.((p1 `2 ) - (p2 `2 )).|)*> by FINSEQ_2: 36

      .= <*( |.((p1 `1 ) - (p2 `1 )).| ^2 ), ( sqrreal . |.((p1 `2 ) - (p2 `2 )).|)*> by RVSUM_1:def 2

      .= <*( |.((p1 `1 ) - (p2 `1 )).| ^2 ), ( |.((p1 `2 ) - (p2 `2 )).| ^2 )*> by RVSUM_1:def 2

      .= <*(((p1 `1 ) - (p2 `1 )) ^2 ), ( |.((p1 `2 ) - (p2 `2 )).| ^2 )*> by COMPLEX1: 75

      .= <*(((p1 `1 ) - (p2 `1 )) ^2 ), (((p1 `2 ) - (p2 `2 )) ^2 )*> by COMPLEX1: 75;

      (( Pitag_dist 2) . (u1,u2)) = |.(v1 - v2).| by EUCLID:def 6

      .= ( sqrt ( Sum ( sqr ( abs (v1 - v2))))) by EUCLID: 25;

      hence thesis by A3, RVSUM_1: 77;

    end;

    theorem :: TOPREAL3:8

    

     Th8: for n be Nat holds the carrier of ( TOP-REAL n) = the carrier of ( Euclid n) by EUCLID: 22;

    reserve lambda for Real;

    theorem :: TOPREAL3:9

    

     Th9: r1 <= s1 implies { p1 : (p1 `1 ) = r & r1 <= (p1 `2 ) & (p1 `2 ) <= s1 } = ( LSeg ( |[r, r1]|, |[r, s1]|))

    proof

      set L = { p3 : (p3 `1 ) = r & r1 <= (p3 `2 ) & (p3 `2 ) <= s1 }, p = |[r, r1]|, q = |[r, s1]|;

      

       A1: (p `1 ) = r by EUCLID: 52;

      assume

       A2: r1 <= s1;

      then

       A3: (s1 - r1) >= (r1 - r1) by XREAL_1: 13;

      

       A4: (q `2 ) = s1 by EUCLID: 52;

      

       A5: (p `2 ) = r1 by EUCLID: 52;

      

       A6: (q `1 ) = r by EUCLID: 52;

      thus L c= ( LSeg (p,q))

      proof

        per cases by A2, XXREAL_0: 1;

          suppose

           A7: r1 = s1;

          L c= {p}

          proof

            let x be object;

            assume x in L;

            then

            consider p2 such that

             A8: x = p2 and

             A9: (p2 `1 ) = r and

             A10: r1 <= (p2 `2 ) & (p2 `2 ) <= s1;

            (p `2 ) = (p2 `2 ) by A5, A7, A10, XXREAL_0: 1;

            then p2 = p by A1, A9, Th6;

            hence thesis by A8, TARSKI:def 1;

          end;

          hence thesis by A7, RLTOPSP1: 70;

        end;

          suppose

           A11: r1 < s1;

          let x be object;

          assume x in L;

          then

          consider p2 such that

           A12: x = p2 and

           A13: (p2 `1 ) = r and

           A14: r1 <= (p2 `2 ) and

           A15: (p2 `2 ) <= s1;

          set t = (p2 `2 ), l = ((t - r1) / (s1 - r1));

          

           A16: (s1 - r1) > 0 by A11, XREAL_1: 50;

          

          then

           A17: (1 - l) = (((1 * (s1 - r1)) - (t - r1)) / (s1 - r1)) by XCMPLX_1: 127

          .= ((s1 - t) / (s1 - r1));

          (t - r1) <= (s1 - r1) by A15, XREAL_1: 9;

          then l <= ((s1 - r1) / (s1 - r1)) by A16, XREAL_1: 72;

          then

           A18: l <= 1 by A16, XCMPLX_1: 60;

          

           A19: ((((1 - l) * p) + (l * q)) `1 ) = ((((1 - l) * p) `1 ) + ((l * q) `1 )) by Th2

          .= (((1 - l) * (p `1 )) + ((l * q) `1 )) by Th4

          .= (((1 - l) * r) + (l * r)) by A1, A6, Th4

          .= (p2 `1 ) by A13;

          ((((1 - l) * p) + (l * q)) `2 ) = ((((1 - l) * p) `2 ) + ((l * q) `2 )) by Th2

          .= (((1 - l) * (p `2 )) + ((l * q) `2 )) by Th4

          .= (((1 - l) * (p `2 )) + (l * (q `2 ))) by Th4

          .= ((((s1 - t) * (p `2 )) / (s1 - r1)) + (l * (q `2 ))) by A17, XCMPLX_1: 74

          .= ((((s1 - t) * (p `2 )) / (s1 - r1)) + (((t - r1) * (q `2 )) / (s1 - r1))) by XCMPLX_1: 74

          .= ((((s1 * r1) - (t * r1)) + ((t - r1) * s1)) / (s1 - r1)) by A5, A4, XCMPLX_1: 62

          .= ((t * (s1 - r1)) / (s1 - r1))

          .= (t * ((s1 - r1) / (s1 - r1))) by XCMPLX_1: 74

          .= (t * 1) by A16, XCMPLX_1: 60

          .= (p2 `2 );

          then

           A20: p2 = (((1 - l) * p) + (l * q)) by A19, Th6;

          (r1 - r1) <= (t - r1) by A14, XREAL_1: 9;

          hence thesis by A16, A12, A18, A20;

        end;

      end;

      let x be object;

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

      then

      consider lambda such that

       A21: (((1 - lambda) * p) + (lambda * q)) = x and

       A22: 0 <= lambda and

       A23: lambda <= 1;

      

       A24: (r1 + 0 ) <= (r1 + (lambda * (s1 - r1))) by A3, A22, XREAL_1: 7;

      (lambda * (s1 - r1)) <= (1 * (s1 - r1)) by A3, A23, XREAL_1: 64;

      then

       A25: (r1 + (lambda * (s1 - r1))) <= ((s1 - r1) + r1) by XREAL_1: 7;

      set p2 = (((1 - lambda) * p) + (lambda * q));

      

       A26: (p2 `2 ) = ((((1 - lambda) * p) `2 ) + ((lambda * q) `2 )) by Th2

      .= (((1 - lambda) * (p `2 )) + ((lambda * q) `2 )) by Th4

      .= (((1 * r1) - (lambda * r1)) + (lambda * s1)) by A5, A4, Th4

      .= (r1 + (lambda * (s1 - r1)));

      (p2 `1 ) = ((((1 - lambda) * p) `1 ) + ((lambda * q) `1 )) by Th2

      .= (((1 - lambda) * (p `1 )) + ((lambda * q) `1 )) by Th4

      .= (((1 - lambda) * r) + (lambda * r)) by A1, A6, Th4

      .= (1 * r);

      hence thesis by A21, A26, A24, A25;

    end;

    theorem :: TOPREAL3:10

    

     Th10: r1 <= s1 implies { p1 : (p1 `2 ) = r & r1 <= (p1 `1 ) & (p1 `1 ) <= s1 } = ( LSeg ( |[r1, r]|, |[s1, r]|))

    proof

      set L = { p3 : (p3 `2 ) = r & r1 <= (p3 `1 ) & (p3 `1 ) <= s1 }, p = |[r1, r]|, q = |[s1, r]|;

      

       A1: (p `1 ) = r1 by EUCLID: 52;

      assume

       A2: r1 <= s1;

      then

       A3: (s1 - r1) >= (r1 - r1) by XREAL_1: 13;

      

       A4: (q `2 ) = r by EUCLID: 52;

      

       A5: (p `2 ) = r by EUCLID: 52;

      

       A6: (q `1 ) = s1 by EUCLID: 52;

      thus L c= ( LSeg (p,q))

      proof

        per cases by A2, XXREAL_0: 1;

          suppose

           A7: r1 = s1;

          L c= {p}

          proof

            let x be object;

            assume x in L;

            then

            consider p2 such that

             A8: x = p2 and

             A9: (p2 `2 ) = r and

             A10: r1 <= (p2 `1 ) & (p2 `1 ) <= s1;

            (p `1 ) = (p2 `1 ) by A1, A7, A10, XXREAL_0: 1;

            then p2 = p by A5, A9, Th6;

            hence thesis by A8, TARSKI:def 1;

          end;

          hence thesis by A7, RLTOPSP1: 70;

        end;

          suppose

           A11: r1 < s1;

          let x be object;

          assume x in L;

          then

          consider p2 such that

           A12: x = p2 and

           A13: (p2 `2 ) = r and

           A14: r1 <= (p2 `1 ) and

           A15: (p2 `1 ) <= s1;

          set t = (p2 `1 ), l = ((t - r1) / (s1 - r1));

          

           A16: (s1 - r1) > 0 by A11, XREAL_1: 50;

          

          then

           A17: (1 - l) = (((1 * (s1 - r1)) - (t - r1)) / (s1 - r1)) by XCMPLX_1: 127

          .= ((s1 - t) / (s1 - r1));

          (t - r1) <= (s1 - r1) by A15, XREAL_1: 9;

          then l <= ((s1 - r1) / (s1 - r1)) by A16, XREAL_1: 72;

          then

           A18: l <= 1 by A16, XCMPLX_1: 60;

          

           A19: ((((1 - l) * p) + (l * q)) `2 ) = ((((1 - l) * p) `2 ) + ((l * q) `2 )) by Th2

          .= (((1 - l) * (p `2 )) + ((l * q) `2 )) by Th4

          .= (((1 - l) * r) + (l * r)) by A5, A4, Th4

          .= (p2 `2 ) by A13;

          ((((1 - l) * p) + (l * q)) `1 ) = ((((1 - l) * p) `1 ) + ((l * q) `1 )) by Th2

          .= (((1 - l) * (p `1 )) + ((l * q) `1 )) by Th4

          .= (((1 - l) * (p `1 )) + (l * (q `1 ))) by Th4

          .= ((((s1 - t) * (p `1 )) / (s1 - r1)) + (l * (q `1 ))) by A17, XCMPLX_1: 74

          .= ((((s1 - t) * (p `1 )) / (s1 - r1)) + (((t - r1) * (q `1 )) / (s1 - r1))) by XCMPLX_1: 74

          .= ((((s1 * r1) - (t * r1)) + ((t - r1) * s1)) / (s1 - r1)) by A1, A6, XCMPLX_1: 62

          .= ((t * (s1 - r1)) / (s1 - r1))

          .= (t * ((s1 - r1) / (s1 - r1))) by XCMPLX_1: 74

          .= (t * 1) by A16, XCMPLX_1: 60

          .= (p2 `1 );

          then

           A20: p2 = (((1 - l) * p) + (l * q)) by A19, Th6;

          (r1 - r1) <= (t - r1) by A14, XREAL_1: 9;

          hence thesis by A16, A12, A18, A20;

        end;

      end;

      let x be object;

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

      then

      consider lambda such that

       A21: (((1 - lambda) * p) + (lambda * q)) = x and

       A22: 0 <= lambda and

       A23: lambda <= 1;

      

       A24: (r1 + 0 ) <= (r1 + (lambda * (s1 - r1))) by A3, A22, XREAL_1: 7;

      (lambda * (s1 - r1)) <= (1 * (s1 - r1)) by A3, A23, XREAL_1: 64;

      then

       A25: (r1 + (lambda * (s1 - r1))) <= ((s1 - r1) + r1) by XREAL_1: 7;

      set p2 = (((1 - lambda) * p) + (lambda * q));

      

       A26: (p2 `1 ) = ((((1 - lambda) * p) `1 ) + ((lambda * q) `1 )) by Th2

      .= (((1 - lambda) * (p `1 )) + ((lambda * q) `1 )) by Th4

      .= (((1 * r1) - (lambda * r1)) + (lambda * s1)) by A1, A6, Th4

      .= (r1 + (lambda * (s1 - r1)));

      (p2 `2 ) = ((((1 - lambda) * p) `2 ) + ((lambda * q) `2 )) by Th2

      .= (((1 - lambda) * (p `2 )) + ((lambda * q) `2 )) by Th4

      .= (((1 - lambda) * r) + (lambda * r)) by A5, A4, Th4

      .= r;

      hence thesis by A21, A26, A24, A25;

    end;

    theorem :: TOPREAL3:11

    p in ( LSeg ( |[r, r1]|, |[r, s1]|)) implies (p `1 ) = r

    proof

      assume

       A1: p in ( LSeg ( |[r, r1]|, |[r, s1]|));

      per cases by XXREAL_0: 1;

        suppose r1 < s1;

        then ( LSeg ( |[r, r1]|, |[r, s1]|)) = { q : (q `1 ) = r & r1 <= (q `2 ) & (q `2 ) <= s1 } by Th9;

        then ex p1 st p1 = p & (p1 `1 ) = r & r1 <= (p1 `2 ) & (p1 `2 ) <= s1 by A1;

        hence thesis;

      end;

        suppose r1 = s1;

        then p in { |[r, r1]|} by A1, RLTOPSP1: 70;

        then p = |[r, r1]| by TARSKI:def 1;

        hence thesis by EUCLID: 52;

      end;

        suppose r1 > s1;

        then ( LSeg ( |[r, r1]|, |[r, s1]|)) = { q : (q `1 ) = r & s1 <= (q `2 ) & (q `2 ) <= r1 } by Th9;

        then ex p1 st p1 = p & (p1 `1 ) = r & s1 <= (p1 `2 ) & (p1 `2 ) <= r1 by A1;

        hence thesis;

      end;

    end;

    theorem :: TOPREAL3:12

    p in ( LSeg ( |[r1, r]|, |[s1, r]|)) implies (p `2 ) = r

    proof

      assume

       A1: p in ( LSeg ( |[r1, r]|, |[s1, r]|));

      per cases by XXREAL_0: 1;

        suppose r1 < s1;

        then ( LSeg ( |[r1, r]|, |[s1, r]|)) = { q : (q `2 ) = r & r1 <= (q `1 ) & (q `1 ) <= s1 } by Th10;

        then ex p1 st p1 = p & (p1 `2 ) = r & r1 <= (p1 `1 ) & (p1 `1 ) <= s1 by A1;

        hence thesis;

      end;

        suppose r1 = s1;

        then p in { |[r1, r]|} by A1, RLTOPSP1: 70;

        then p = |[r1, r]| by TARSKI:def 1;

        hence thesis by EUCLID: 52;

      end;

        suppose r1 > s1;

        then ( LSeg ( |[r1, r]|, |[s1, r]|)) = { q : (q `2 ) = r & s1 <= (q `1 ) & (q `1 ) <= r1 } by Th10;

        then ex p1 st p1 = p & (p1 `2 ) = r & s1 <= (p1 `1 ) & (p1 `1 ) <= r1 by A1;

        hence thesis;

      end;

    end;

    theorem :: TOPREAL3:13

    (p `1 ) <> (q `1 ) & (p `2 ) = (q `2 ) implies |[(((p `1 ) + (q `1 )) / 2), (p `2 )]| in ( LSeg (p,q))

    proof

      set p1 = |[(((p `1 ) + (q `1 )) / 2), (p `2 )]|;

      assume that

       A1: (p `1 ) <> (q `1 ) and

       A2: (p `2 ) = (q `2 );

      

       A3: p = |[(p `1 ), (p `2 )]| & q = |[(q `1 ), (p `2 )]| by A2, EUCLID: 53;

      

       A4: (p1 `1 ) = (((p `1 ) + (q `1 )) / 2) & (p1 `2 ) = (p `2 ) by EUCLID: 52;

      per cases by A1, XXREAL_0: 1;

        suppose

         A5: (p `1 ) < (q `1 );

        then (p `1 ) <= (((p `1 ) + (q `1 )) / 2) & (((p `1 ) + (q `1 )) / 2) <= (q `1 ) by XREAL_1: 226;

        then p1 in { p2 : (p2 `2 ) = (p `2 ) & (p `1 ) <= (p2 `1 ) & (p2 `1 ) <= (q `1 ) } by A4;

        hence thesis by A3, A5, Th10;

      end;

        suppose

         A6: (p `1 ) > (q `1 );

        then (q `1 ) <= (((p `1 ) + (q `1 )) / 2) & (((p `1 ) + (q `1 )) / 2) <= (p `1 ) by XREAL_1: 226;

        then p1 in { p2 : (p2 `2 ) = (p `2 ) & (q `1 ) <= (p2 `1 ) & (p2 `1 ) <= (p `1 ) } by A4;

        hence thesis by A3, A6, Th10;

      end;

    end;

    theorem :: TOPREAL3:14

    (p `1 ) = (q `1 ) & (p `2 ) <> (q `2 ) implies |[(p `1 ), (((p `2 ) + (q `2 )) / 2)]| in ( LSeg (p,q))

    proof

      set p1 = |[(p `1 ), (((p `2 ) + (q `2 )) / 2)]|;

      assume that

       A1: (p `1 ) = (q `1 ) and

       A2: (p `2 ) <> (q `2 );

      

       A3: p = |[(p `1 ), (p `2 )]| & q = |[(p `1 ), (q `2 )]| by A1, EUCLID: 53;

      

       A4: (p1 `1 ) = (p `1 ) & (p1 `2 ) = (((p `2 ) + (q `2 )) / 2) by EUCLID: 52;

      per cases by A2, XXREAL_0: 1;

        suppose

         A5: (p `2 ) < (q `2 );

        then (p `2 ) <= (((p `2 ) + (q `2 )) / 2) & (((p `2 ) + (q `2 )) / 2) <= (q `2 ) by XREAL_1: 226;

        then p1 in { p2 : (p2 `1 ) = (p `1 ) & (p `2 ) <= (p2 `2 ) & (p2 `2 ) <= (q `2 ) } by A4;

        hence thesis by A3, A5, Th9;

      end;

        suppose

         A6: (p `2 ) > (q `2 );

        then (q `2 ) <= (((p `2 ) + (q `2 )) / 2) & (((p `2 ) + (q `2 )) / 2) <= (p `2 ) by XREAL_1: 226;

        then p1 in { p2 : (p2 `1 ) = (p `1 ) & (q `2 ) <= (p2 `2 ) & (p2 `2 ) <= (p `2 ) } by A4;

        hence thesis by A3, A6, Th9;

      end;

    end;

    theorem :: TOPREAL3:15

    

     Th15: for i,j be Nat holds f = <*p, p1, q*> & i <> 0 & j > (i + 1) implies ( LSeg (f,j)) = {}

    proof

      let i,j be Nat;

      assume that

       A1: f = <*p, p1, q*> and

       A2: i <> 0 and

       A3: j > (i + 1);

      i >= ( 0 + 1) by A2, NAT_1: 13;

      then (1 + i) >= (1 + 1) by XREAL_1: 7;

      then j > 2 by A3, XXREAL_0: 2;

      then j >= (2 + 1) by NAT_1: 13;

      then

       A4: (j + 1) > 3 by NAT_1: 13;

      ( len f) = 3 by A1, FINSEQ_1: 45;

      hence thesis by A4, TOPREAL1:def 3;

    end;

    theorem :: TOPREAL3:16

    f = <*p1, p2, p3*> implies ( L~ f) = (( LSeg (p1,p2)) \/ ( LSeg (p2,p3)))

    proof

      set M = { ( LSeg (f,i)) : 1 <= i & (i + 1) <= ( len f) };

      assume

       A1: f = <*p1, p2, p3*>;

      then

       A2: ( len f) = (2 + 1) by FINSEQ_1: 45;

      

       A3: (f /. 3) = p3 by A1, FINSEQ_4: 18;

      

       A4: (f /. 1) = p1 by A1, FINSEQ_4: 18;

      

       A5: (f /. 2) = p2 by A1, FINSEQ_4: 18;

      

       A6: (1 + 1) in ( dom f) by A1, Th1;

      M = {( LSeg (p1,p2)), ( LSeg (p2,p3))}

      proof

        thus M c= {( LSeg (p1,p2)), ( LSeg (p2,p3))}

        proof

          let x be object;

          assume x in M;

          then

          consider j such that

           A7: x = ( LSeg (f,j)) and

           A8: 1 <= j and

           A9: (j + 1) <= ( len f);

          j <= 2 by A2, A9, XREAL_1: 6;

          then j = 0 or ... or j = 2;

          per cases by A8;

            suppose j = 1;

            then x = ( LSeg (p1,p2)) by A4, A5, A7, A9, TOPREAL1:def 3;

            hence thesis by TARSKI:def 2;

          end;

            suppose j = 2;

            then x = ( LSeg (p2,p3)) by A2, A5, A3, A7, TOPREAL1:def 3;

            hence thesis by TARSKI:def 2;

          end;

        end;

        let x be object such that

         A10: x in {( LSeg (p1,p2)), ( LSeg (p2,p3))};

        per cases by A10, TARSKI:def 2;

          suppose

           A11: x = ( LSeg (p1,p2));

          

           A12: (1 + 1) <= ( len f) by A2;

          x = ( LSeg (f,1)) by A2, A4, A5, A6, A11, TOPREAL1:def 3;

          hence thesis by A12;

        end;

          suppose x = ( LSeg (p2,p3));

          then x = ( LSeg (f,2)) by A2, A5, A3, TOPREAL1:def 3;

          hence thesis by A2;

        end;

      end;

      hence thesis by ZFMISC_1: 75;

    end;

    theorem :: TOPREAL3:17

    

     Th17: j in ( dom (f | i)) & (j + 1) in ( dom (f | i)) implies ( LSeg (f,j)) = ( LSeg ((f | i),j))

    proof

      assume that

       A1: j in ( dom (f | i)) and

       A2: (j + 1) in ( dom (f | i));

      

       A3: 1 <= j & (j + 1) <= ( len (f | i)) by A1, A2, FINSEQ_3: 25;

      set p1 = ((f | i) /. j), p2 = ((f | i) /. (j + 1));

      

       A4: (f | i) = (f | ( Seg i)) by FINSEQ_1:def 15;

      then j in (( dom f) /\ ( Seg i)) by A1, RELAT_1: 61;

      then j in ( dom f) by XBOOLE_0:def 4;

      then

       A5: 1 <= j by FINSEQ_3: 25;

      (j + 1) in (( dom f) /\ ( Seg i)) by A2, A4, RELAT_1: 61;

      then (j + 1) in ( dom f) by XBOOLE_0:def 4;

      then

       A6: (j + 1) <= ( len f) by FINSEQ_3: 25;

      p1 = (f /. j) & p2 = (f /. (j + 1)) by A1, A2, FINSEQ_4: 70;

      then ( LSeg (f,j)) = ( LSeg (p1,p2)) by A5, A6, TOPREAL1:def 3;

      hence thesis by A3, TOPREAL1:def 3;

    end;

    theorem :: TOPREAL3:18

    j in ( dom f) & (j + 1) in ( dom f) implies ( LSeg ((f ^ h),j)) = ( LSeg (f,j))

    proof

      assume that

       A1: j in ( dom f) and

       A2: (j + 1) in ( dom f);

      

       A3: 1 <= j & (j + 1) <= ( len f) by A1, A2, FINSEQ_3: 25;

      ( dom f) c= ( dom (f ^ h)) by FINSEQ_1: 26;

      then

       A4: (j + 1) <= ( len (f ^ h)) by A2, FINSEQ_3: 25;

      set p1 = (f /. j), p2 = (f /. (j + 1));

      

       A5: 1 <= j by A1, FINSEQ_3: 25;

      p1 = ((f ^ h) /. j) & p2 = ((f ^ h) /. (j + 1)) by A1, A2, FINSEQ_4: 68;

      then ( LSeg ((f ^ h),j)) = ( LSeg (p1,p2)) by A5, A4, TOPREAL1:def 3;

      hence thesis by A3, TOPREAL1:def 3;

    end;

    theorem :: TOPREAL3:19

    

     Th19: for f be FinSequence of ( TOP-REAL n), i be Nat holds ( LSeg (f,i)) c= ( L~ f)

    proof

      let f be FinSequence of ( TOP-REAL n), i be Nat;

      let x be object such that

       A1: x in ( LSeg (f,i));

      now

        per cases ;

          case i < 1;

          hence contradiction by A1, TOPREAL1:def 3;

        end;

          case

           A2: i >= 1;

          now

            per cases ;

              case (i + 1) > ( len f);

              hence contradiction by A1, TOPREAL1:def 3;

            end;

              case

               A3: (i + 1) <= ( len f);

              set M = { ( LSeg (f,j)) : 1 <= j & (j + 1) <= ( len f) };

              ( LSeg (f,i)) in M by A2, A3;

              hence thesis by A1, TARSKI:def 4;

            end;

          end;

          hence thesis;

        end;

      end;

      hence thesis;

    end;

    theorem :: TOPREAL3:20

    ( L~ (f | i)) c= ( L~ f)

    proof

      set h = (f | i), Mh = { ( LSeg (h,n)) : 1 <= n & (n + 1) <= ( len h) }, Mf = { ( LSeg (f,m)) : 1 <= m & (m + 1) <= ( len f) };

      let x be object;

      

       A1: h = (f | ( Seg i)) by FINSEQ_1:def 15;

      

       A2: ( dom f) = ( Seg ( len f)) by FINSEQ_1:def 3;

      assume

       A3: x in ( L~ h);

      then

      consider X be set such that

       A4: x in X and

       A5: X in Mh by TARSKI:def 4;

      consider k such that

       A6: X = ( LSeg (h,k)) and

       A7: 1 <= k and

       A8: (k + 1) <= ( len h) by A5;

      per cases ;

        suppose

         A9: i in ( dom f);

        

         A10: ( dom h) = (( dom f) /\ ( Seg i)) by A1, RELAT_1: 61;

        

         A11: i in NAT by ORDINAL1:def 12;

        

         A12: i <= ( len f) by A9, FINSEQ_3: 25;

        then ( Seg i) c= ( dom f) by A2, FINSEQ_1: 5;

        then ( dom h) = ( Seg i) by A10, XBOOLE_1: 28;

        then ( len h) <= ( len f) by A12, A11, FINSEQ_1:def 3;

        then

         A13: (k + 1) <= ( len f) by A8, XXREAL_0: 2;

        k <= (k + 1) by NAT_1: 12;

        then k <= ( len h) by A8, XXREAL_0: 2;

        then

         A14: k in ( dom h) by A7, FINSEQ_3: 25;

        1 <= (k + 1) by NAT_1: 12;

        then (k + 1) in ( dom h) by A8, FINSEQ_3: 25;

        then X = ( LSeg (f,k)) by A6, A14, Th17;

        then X in Mf by A7, A13;

        hence thesis by A4, TARSKI:def 4;

      end;

        suppose

         A15: not i in ( dom f);

        now

          per cases by A15, FINSEQ_3: 25;

            case i < 1;

            then i < ( 0 + 1);

            then i <= 0 by NAT_1: 13;

            then ( Seg i) = {} ;

            then ( dom h) = (( dom f) /\ {} ) by A1, RELAT_1: 61;

            then ( dom h) = {} ;

            then ( Seg ( len h)) = {} by FINSEQ_1:def 3;

            then ( len h) = 0 ;

            hence contradiction by A3, TOPREAL1: 22;

          end;

            case ( len f) < i;

            then ( Seg ( len f)) c= ( Seg i) by FINSEQ_1: 5;

            then ( dom f) c= ( Seg i) by FINSEQ_1:def 3;

            then

             A16: ( dom f) = (( dom f) /\ ( Seg i)) by XBOOLE_1: 28;

            for x be object st x in ( dom h) holds (h . x) = (f . x) by A1, FUNCT_1: 47;

            then h = f by A1, A16, RELAT_1: 61;

            hence thesis by A4, A5, TARSKI:def 4;

          end;

        end;

        hence thesis;

      end;

    end;

    theorem :: TOPREAL3:21

    

     Th21: for p1,p2 be Point of ( TOP-REAL N), u be Point of ( Euclid N) st p1 in ( Ball (u,r)) & p2 in ( Ball (u,r)) holds ( LSeg (p1,p2)) c= ( Ball (u,r))

    proof

      let p1,p2 be Point of ( TOP-REAL N), u be Point of ( Euclid N);

      assume that

       A1: p1 in ( Ball (u,r)) and

       A2: p2 in ( Ball (u,r));

      reconsider p9 = p1 as Point of ( Euclid N) by A1;

      

       A3: ( dist (p9,u)) < r by A1, METRIC_1: 11;

      thus ( LSeg (p1,p2)) c= ( Ball (u,r))

      proof

        p2 in { u4 where u4 be Point of ( Euclid N) : ( dist (u,u4)) < r } by A2, METRIC_1: 17;

        then

         A4: ex u4 be Point of ( Euclid N) st u4 = p2 & ( dist (u,u4)) < r;

        reconsider q29 = u as Element of ( REAL N);

        let a be object;

        reconsider q2 = q29 as Point of ( TOP-REAL N) by EUCLID: 22;

        assume a in ( LSeg (p1,p2));

        then

        consider lambda such that

         A5: (((1 - lambda) * p1) + (lambda * p2)) = a and

         A6: 0 <= lambda and

         A7: lambda <= 1;

        

         A8: lambda = |.lambda.| by A6, ABSVALUE:def 1;

        set p = (((1 - lambda) * p1) + (lambda * p2));

        reconsider p9 = p, p19 = p1, p29 = p2 as Element of ( REAL N) by EUCLID: 22;

        reconsider u5 = (((1 - lambda) * p1) + (lambda * p2)) as Point of ( Euclid N) by EUCLID: 22;

        

         A9: (( Pitag_dist N) . (q29,p9)) = |.(q29 - p9).| & (( Pitag_dist N) . (u,u5)) = ( dist (u,u5)) by EUCLID:def 6, METRIC_1:def 1;

        (( Pitag_dist N) . (q29,p29)) = |.(q29 - p29).| by EUCLID:def 6;

        then

         A10: |.(q29 + ( - p29)).| < r by A4, METRIC_1:def 1;

        

         A11: 0 <= (1 - lambda) by A7, XREAL_1: 48;

        then

         A12: (1 - lambda) = |.(1 - lambda).| by ABSVALUE:def 1;

        consider u3 be Point of ( Euclid N) such that

         A13: u3 = p1 and

         A14: ( dist (u,u3)) < r by A3;

        

         A15: (( Pitag_dist N) . (q29,p19)) = |.(q29 - p19).| by EUCLID:def 6;

        then

         A16: ( dist (u,u3)) = |.(q29 - p19).| by A13, METRIC_1:def 1;

        ( |.(1 - lambda).| * |.(q29 + ( - p19)).|) < ((1 - lambda) * r) & ( |.lambda.| * |.(q29 + ( - p29)).|) <= (lambda * r) or ( |.(1 - lambda).| * |.(q29 + ( - p19)).|) <= ((1 - lambda) * r) & ( |.lambda.| * |.(q29 + ( - p29)).|) < (lambda * r)

        proof

          per cases by A6;

            suppose lambda = 0 ;

            hence thesis by A13, A14, A15, A12, A8, METRIC_1:def 1;

          end;

            suppose lambda > 0 ;

            hence thesis by A14, A16, A10, A11, A12, A8, XREAL_1: 64, XREAL_1: 68;

          end;

        end;

        then

         A17: (( |.(1 - lambda).| * |.(q29 + ( - p19)).|) + ( |.lambda.| * |.(q29 + ( - p29)).|)) < (((1 - lambda) * r) + (lambda * r)) by XREAL_1: 8;

        (q29 - p19) = (q2 - p1) by EUCLID: 69;

        then

         A18: (q29 - p9) = (q2 - p) & ((1 - lambda) * (q29 - p19)) = ((1 - lambda) * (q2 - p1)) by EUCLID: 65, EUCLID: 69;

        (q29 - p29) = (q2 - p2) by EUCLID: 69;

        then

         A19: (lambda * (q29 - p29)) = (lambda * (q2 - p2)) by EUCLID: 65;

        (q2 - p) = ((((1 - lambda) + lambda) * q2) - (((1 - lambda) * p1) + (lambda * p2))) by RLVECT_1:def 8

        .= ((((1 - lambda) * q2) + (lambda * q2)) - (((1 - lambda) * p1) + (lambda * p2))) by RLVECT_1:def 6

        .= ((((1 - lambda) * q2) + (lambda * q2)) + ( - (((1 - lambda) * p1) + (lambda * p2))))

        .= ((((1 - lambda) * q2) + (lambda * q2)) + (( - ((1 - lambda) * p1)) - (lambda * p2))) by RLVECT_1: 30

        .= (((((1 - lambda) * q2) + (lambda * q2)) + ( - ((1 - lambda) * p1))) + ( - (lambda * p2))) by RLVECT_1:def 3

        .= (((((1 - lambda) * q2) + ( - ((1 - lambda) * p1))) + (lambda * q2)) + ( - (lambda * p2))) by RLVECT_1:def 3

        .= (((((1 - lambda) * q2) + ((1 - lambda) * ( - p1))) + (lambda * q2)) + ( - (lambda * p2))) by RLVECT_1: 25

        .= ((((1 - lambda) * (q2 + ( - p1))) + (lambda * q2)) + ( - (lambda * p2))) by RLVECT_1:def 5

        .= (((1 - lambda) * (q2 + ( - p1))) + ((lambda * q2) + ( - (lambda * p2)))) by RLVECT_1:def 3

        .= (((1 - lambda) * (q2 + ( - p1))) + ((lambda * q2) + (lambda * ( - p2)))) by RLVECT_1: 25

        .= (((1 - lambda) * (q2 - p1)) + (lambda * (q2 - p2))) by RLVECT_1:def 5;

        then (q29 - p9) = (((1 - lambda) * (q29 - p19)) + (lambda * (q29 - p29))) by A18, A19, EUCLID: 64;

        then

         A20: |.(q29 - p9).| <= ( |.((1 - lambda) * (q29 - p19)).| + |.(lambda * (q29 - p29)).|) by EUCLID: 12;

        ( |.((1 - lambda) * (q29 + ( - p19))).| + |.(lambda * (q29 + ( - p29))).|) = (( |.(1 - lambda).| * |.(q29 + ( - p19)).|) + |.(lambda * (q29 + ( - p29))).|) by EUCLID: 11

        .= (( |.(1 - lambda).| * |.(q29 + ( - p19)).|) + ( |.lambda.| * |.(q29 + ( - p29)).|)) by EUCLID: 11;

        then |.(q29 - p9).| < r by A20, A17, XXREAL_0: 2;

        then a in { u6 where u6 be Element of ( Euclid N) : ( dist (u,u6)) < r } by A5, A9;

        hence thesis by METRIC_1: 17;

      end;

    end;

    theorem :: TOPREAL3:22

    u = p1 & p1 = |[r1, s1]| & p2 = |[r2, s2]| & p = |[r2, s1]| & p2 in ( Ball (u,r)) implies p in ( Ball (u,r))

    proof

      assume that

       A1: u = p1 and

       A2: p1 = |[r1, s1]| and

       A3: p2 = |[r2, s2]| and

       A4: p = |[r2, s1]| and

       A5: p2 in ( Ball (u,r));

      reconsider p19 = p1, p29 = p2, p9 = p as Element of ( REAL 2) by EUCLID: 22;

      reconsider r1, s1, r2, s2 as Real;

      

       A6: (( Pitag_dist 2) . (p19,p29)) = |.(p19 - p29).| by EUCLID:def 6;

      p2 in { u6 where u6 be Element of ( Euclid 2) : ( dist (u,u6)) < r } by A5, METRIC_1: 17;

      then ex u5 st u5 = p2 & ( dist (u,u5)) < r;

      then

       A7: |.(p19 - p29).| < r by A1, A6, METRIC_1:def 1;

      reconsider up = p as Point of ( Euclid 2) by EUCLID: 22;

      (( Pitag_dist 2) . (p19,p9)) = |.(p19 - p9).| by EUCLID:def 6;

      then

       A8: ( dist (u,up)) = |.(p19 - p9).| by A1, METRIC_1:def 1;

      ((s1 - s2) ^2 ) >= 0 by XREAL_1: 63;

      then ( sqrreal . (s1 - s2)) >= 0 by RVSUM_1:def 2;

      then

       A9: (( sqrreal . (r1 - r2)) + 0 ) <= (( sqrreal . (r1 - r2)) + ( sqrreal . (s1 - s2))) by XREAL_1: 7;

      (p19 - p9) = (p1 - p) by EUCLID: 69;

      then (p19 - p9) = <*(r1 - r2), (s1 - s1)*> by A2, A4, Th5;

      then ( sqr (p19 - p9)) = <*( sqrreal . (r1 - r2)), ( sqrreal . (s1 - s1))*> by FINSEQ_2: 36;

      

      then

       A10: ( Sum ( sqr (p19 - p9))) = (( sqrreal . (r1 - r2)) + ( sqrreal . 0 )) by RVSUM_1: 77

      .= (( sqrreal . (r1 - r2)) + ( 0 ^2 )) by RVSUM_1:def 2

      .= ( sqrreal . (r1 - r2));

      (p19 - p29) = (p1 - p2) by EUCLID: 69;

      then (p19 - p29) = <*(r1 - r2), (s1 - s2)*> by A2, A3, Th5;

      then ( sqr (p19 - p29)) = <*( sqrreal . (r1 - r2)), ( sqrreal . (s1 - s2))*> by FINSEQ_2: 36;

      then

       A11: |.(p19 - p29).| = ( sqrt (( sqrreal . (r1 - r2)) + ( sqrreal . (s1 - s2)))) by RVSUM_1: 77;

      ((r1 - r2) ^2 ) >= 0 by XREAL_1: 63;

      then ( sqrreal . (r1 - r2)) >= 0 by RVSUM_1:def 2;

      then |.(p19 - p9).| <= ( sqrt (( sqrreal . (r1 - r2)) + ( sqrreal . (s1 - s2)))) by A10, A9, SQUARE_1: 26;

      then |.(p19 - p9).| < r by A7, A11, XXREAL_0: 2;

      then p in { u6 where u6 be Element of ( Euclid 2) : ( dist (u,u6)) < r } by A8;

      hence thesis by METRIC_1: 17;

    end;

    theorem :: TOPREAL3:23

     |[s, r1]| in ( Ball (u,r)) & |[s, s1]| in ( Ball (u,r)) implies |[s, ((r1 + s1) / 2)]| in ( Ball (u,r))

    proof

      set p = |[s, r1]|, q = |[s, s1]|, p3 = |[s, ((r1 + s1) / 2)]|;

      assume |[s, r1]| in ( Ball (u,r)) & |[s, s1]| in ( Ball (u,r));

      then

       A1: ( LSeg ( |[s, r1]|, |[s, s1]|)) c= ( Ball (u,r)) by Th21;

      (p `2 ) = r1 & (q `2 ) = s1 by EUCLID: 52;

      

      then

       A2: (p3 `2 ) = (((1 - (1 / 2)) * (p `2 )) + ((1 / 2) * (q `2 ))) by EUCLID: 52

      .= ((((1 - (1 / 2)) * p) `2 ) + ((1 / 2) * (q `2 ))) by Th4

      .= ((((1 - (1 / 2)) * p) `2 ) + (((1 / 2) * q) `2 )) by Th4

      .= ((((1 - (1 / 2)) * p) + ((1 / 2) * q)) `2 ) by Th2;

      (p `1 ) = s & (q `1 ) = s by EUCLID: 52;

      

      then (p3 `1 ) = (((1 - (1 / 2)) * (p `1 )) + ((1 / 2) * (q `1 ))) by EUCLID: 52

      .= ((((1 - (1 / 2)) * p) `1 ) + ((1 / 2) * (q `1 ))) by Th4

      .= ((((1 - (1 / 2)) * p) `1 ) + (((1 / 2) * q) `1 )) by Th4

      .= ((((1 - (1 / 2)) * p) + ((1 / 2) * q)) `1 ) by Th2;

      then p3 = (((1 - (1 / 2)) * p) + ((1 / 2) * q)) by A2, Th6;

      then p3 in { (((1 - lambda) * p) + (lambda * q)) : 0 <= lambda & lambda <= 1 };

      hence thesis by A1;

    end;

    theorem :: TOPREAL3:24

     |[r1, s]| in ( Ball (u,r)) & |[s1, s]| in ( Ball (u,r)) implies |[((r1 + s1) / 2), s]| in ( Ball (u,r))

    proof

      set p = |[r1, s]|, q = |[s1, s]|, p3 = |[((r1 + s1) / 2), s]|;

      assume |[r1, s]| in ( Ball (u,r)) & |[s1, s]| in ( Ball (u,r));

      then

       A1: ( LSeg ( |[r1, s]|, |[s1, s]|)) c= ( Ball (u,r)) by Th21;

      (p `1 ) = r1 & (q `1 ) = s1 by EUCLID: 52;

      

      then

       A2: (p3 `1 ) = (((1 - (1 / 2)) * (p `1 )) + ((1 / 2) * (q `1 ))) by EUCLID: 52

      .= ((((1 - (1 / 2)) * p) `1 ) + ((1 / 2) * (q `1 ))) by Th4

      .= ((((1 - (1 / 2)) * p) `1 ) + (((1 / 2) * q) `1 )) by Th4

      .= ((((1 - (1 / 2)) * p) + ((1 / 2) * q)) `1 ) by Th2;

      (p `2 ) = s & (q `2 ) = s by EUCLID: 52;

      

      then (p3 `2 ) = (((1 - (1 / 2)) * (p `2 )) + ((1 / 2) * (q `2 ))) by EUCLID: 52

      .= ((((1 - (1 / 2)) * p) `2 ) + ((1 / 2) * (q `2 ))) by Th4

      .= ((((1 - (1 / 2)) * p) `2 ) + (((1 / 2) * q) `2 )) by Th4

      .= ((((1 - (1 / 2)) * p) + ((1 / 2) * q)) `2 ) by Th2;

      then p3 = (((1 - (1 / 2)) * p) + ((1 / 2) * q)) by A2, Th6;

      then p3 in { (((1 - lambda) * p) + (lambda * q)) : 0 <= lambda & lambda <= 1 };

      hence thesis by A1;

    end;

    theorem :: TOPREAL3:25

     |[r1, r2]| in ( Ball (u,r)) & |[s1, s2]| in ( Ball (u,r)) implies |[r1, s2]| in ( Ball (u,r)) or |[s1, r2]| in ( Ball (u,r))

    proof

      assume that

       A1: |[r1, r2]| in ( Ball (u,r)) and

       A2: |[s1, s2]| in ( Ball (u,r));

      

       A3: r > 0 by A1, TBSP_1: 12;

      per cases ;

        suppose |[r1, s2]| in ( Ball (u,r));

        hence thesis;

      end;

        suppose

         A4: not |[r1, s2]| in ( Ball (u,r));

        reconsider p = u as Point of ( TOP-REAL 2) by EUCLID: 22;

        set p1 = |[r1, s2]|, p2 = |[s1, r2]|, p3 = |[s1, s2]|, p4 = |[r1, r2]|;

        reconsider u1 = p1, u2 = p2, u3 = p3, u4 = p4 as Point of ( Euclid 2) by EUCLID: 22;

        set a = ((((p `1 ) - (p1 `1 )) ^2 ) + (((p `2 ) - (p1 `2 )) ^2 )), b = ((((p `1 ) - (p4 `1 )) ^2 ) + (((p `2 ) - (p4 `2 )) ^2 )), c = ((((p `1 ) - (p3 `1 )) ^2 ) + (((p `2 ) - (p3 `2 )) ^2 )), d = ((((p `1 ) - (p2 `1 )) ^2 ) + (((p `2 ) - (p2 `2 )) ^2 ));

        (( Pitag_dist 2) . (u,u1)) = ( dist (u,u1)) & r <= ( dist (u,u1)) by A4, METRIC_1: 11, METRIC_1:def 1;

        then r <= ( sqrt a) by Th7;

        then

         A5: (r * r) <= (( sqrt a) ^2 ) by A3, XREAL_1: 66;

        (((p `1 ) - (p1 `1 )) ^2 ) >= 0 & (((p `2 ) - (p1 `2 )) ^2 ) >= 0 by XREAL_1: 63;

        then

         A6: (r ^2 ) <= a by A5, SQUARE_1:def 2;

        

         A7: (p2 `1 ) = s1 & (p2 `2 ) = r2 by EUCLID: 52;

        

         A8: (p4 `1 ) = r1 & (p4 `2 ) = r2 by EUCLID: 52;

        

         A9: (p3 `1 ) = s1 & (p3 `2 ) = s2 by EUCLID: 52;

        (( Pitag_dist 2) . (u,u3)) = ( dist (u,u3)) & ( dist (u,u3)) < r by A2, METRIC_1: 11, METRIC_1:def 1;

        then

         A10: ( sqrt c) < r by Th7;

        

         A11: (((p `1 ) - (p3 `1 )) ^2 ) >= 0 & (((p `2 ) - (p3 `2 )) ^2 ) >= 0 by XREAL_1: 63;

        then 0 <= ( sqrt c) by SQUARE_1:def 2;

        then (( sqrt c) ^2 ) < (r * r) by A10, XREAL_1: 96;

        then

         A12: c < (r * r) by A11, SQUARE_1:def 2;

        (( Pitag_dist 2) . (u,u4)) = ( dist (u,u4)) & ( dist (u,u4)) < r by A1, METRIC_1: 11, METRIC_1:def 1;

        then

         A13: ( sqrt b) < r by Th7;

        (p1 `1 ) = r1 & (p1 `2 ) = s2 by EUCLID: 52;

        then (c + b) = (a + d) by A7, A9, A8;

        then

         A14: ((r ^2 ) + d) <= (c + b) by A6, XREAL_1: 6;

        

         A15: (((p `1 ) - (p4 `1 )) ^2 ) >= 0 & (((p `2 ) - (p4 `2 )) ^2 ) >= 0 by XREAL_1: 63;

        then 0 <= ( sqrt b) by SQUARE_1:def 2;

        then (( sqrt b) ^2 ) < (r * r) by A13, XREAL_1: 96;

        then b < (r ^2 ) by A15, SQUARE_1:def 2;

        then (c + b) < ((r ^2 ) + (r ^2 )) by A12, XREAL_1: 8;

        then ((r ^2 ) + d) < ((r ^2 ) + (r ^2 )) by A14, XXREAL_0: 2;

        then

         A16: d < (((r ^2 ) + (r ^2 )) - (r ^2 )) by XREAL_1: 20;

        (((p `1 ) - (p2 `1 )) ^2 ) >= 0 & (((p `2 ) - (p2 `2 )) ^2 ) >= 0 by XREAL_1: 63;

        then ( sqrt d) < ( sqrt (r ^2 )) by A16, SQUARE_1: 27;

        then

         A17: ( sqrt d) < r by A3, SQUARE_1: 22;

        ( dist (u,u2)) = (( Pitag_dist 2) . (u,u2)) by METRIC_1:def 1

        .= ( sqrt d) by Th7;

        hence thesis by A17, METRIC_1: 11;

      end;

    end;

    theorem :: TOPREAL3:26

     not (f /. 1) in ( Ball (u,r)) & 1 <= m & m <= (( len f) - 1) & (for i st 1 <= i & i <= (( len f) - 1) & (( LSeg (f,i)) /\ ( Ball (u,r))) <> {} holds m <= i) implies not (f /. m) in ( Ball (u,r))

    proof

      assume that

       A1: not (f /. 1) in ( Ball (u,r)) and

       A2: 1 <= m and

       A3: m <= (( len f) - 1) and

       A4: for i st 1 <= i & i <= (( len f) - 1) & (( LSeg (f,i)) /\ ( Ball (u,r))) <> {} holds m <= i;

      assume

       A5: (f /. m) in ( Ball (u,r));

      per cases by A2, XXREAL_0: 1;

        suppose 1 = m;

        hence contradiction by A1, A5;

      end;

        suppose

         A6: 1 < m;

        reconsider k = (m - 1) as Element of NAT by A6, INT_1: 5;

        (1 + 1) <= m by A6, NAT_1: 13;

        then

         A7: 1 <= (m - 1) by XREAL_1: 19;

        (m - 1) <= m by XREAL_1: 43;

        then

         A8: k <= (( len f) - 1) by A3, XXREAL_0: 2;

        then (k + 1) <= ( len f) by XREAL_1: 19;

        then (f /. (k + 1)) in ( LSeg (f,k)) by A7, TOPREAL1: 21;

        then (( LSeg (f,k)) /\ ( Ball (u,r))) <> {} by A5, XBOOLE_0:def 4;

        then m <= k by A4, A7, A8;

        then (m + 1) <= m by XREAL_1: 19;

        hence contradiction by NAT_1: 13;

      end;

    end;

    theorem :: TOPREAL3:27

    for q, p2, p st (q `2 ) = (p2 `2 ) & (p `2 ) <> (p2 `2 ) holds ((( LSeg (p2, |[(p2 `1 ), (p `2 )]|)) \/ ( LSeg ( |[(p2 `1 ), (p `2 )]|,p))) /\ ( LSeg (q,p2))) = {p2}

    proof

      let q, p2, p such that

       A1: (q `2 ) = (p2 `2 ) and

       A2: (p `2 ) <> (p2 `2 );

      set p3 = |[(p2 `1 ), (p `2 )]|;

      set l23 = ( LSeg (p2,p3)), l3 = ( LSeg (p3,p)), l = ( LSeg (q,p2));

      

       A3: (l3 /\ l) = {}

      proof

        set x = the Element of (l3 /\ l);

        assume

         A4: (l3 /\ l) <> {} ;

        then x in l3 by XBOOLE_0:def 4;

        then

        consider s1 be Real such that

         A5: x = (((1 - s1) * p3) + (s1 * p)) and 0 <= s1 and s1 <= 1;

        x in l by A4, XBOOLE_0:def 4;

        then

        consider s2 be Real such that

         A6: x = (((1 - s2) * q) + (s2 * p2)) and 0 <= s2 and s2 <= 1;

        

         A7: ((((1 - s1) * p3) + (s1 * p)) `2 ) = ((((1 - s1) * p3) `2 ) + ((s1 * p) `2 )) by Th2

        .= (((1 - s1) * (p3 `2 )) + ((s1 * p) `2 )) by Th4

        .= (((1 - s1) * (p3 `2 )) + (s1 * (p `2 ))) by Th4

        .= (((1 - s1) * (p `2 )) + (s1 * (p `2 ))) by EUCLID: 52

        .= (p `2 );

        ((((1 - s2) * q) + (s2 * p2)) `2 ) = ((((1 - s2) * q) `2 ) + ((s2 * p2) `2 )) by Th2

        .= (((1 - s2) * (q `2 )) + ((s2 * p2) `2 )) by Th4

        .= (((1 - s2) * (q `2 )) + (s2 * (p2 `2 ))) by Th4

        .= (p2 `2 ) by A1;

        hence contradiction by A2, A5, A7, A6;

      end;

      

       A8: (l23 /\ l) = {p2}

      proof

        thus (l23 /\ l) c= {p2}

        proof

          let x be object;

          assume

           A9: x in (l23 /\ l);

          then x in l23 by XBOOLE_0:def 4;

          then

          consider s1 be Real such that

           A10: (((1 - s1) * p2) + (s1 * p3)) = x and 0 <= s1 and s1 <= 1;

          x in l by A9, XBOOLE_0:def 4;

          then

          consider s2 be Real such that

           A11: (((1 - s2) * q) + (s2 * p2)) = x and 0 <= s2 and s2 <= 1;

          

           A12: ((((1 - s2) * q) + (s2 * p2)) `2 ) = ((((1 - s2) * q) `2 ) + ((s2 * p2) `2 )) by Th2

          .= (((1 - s2) * (q `2 )) + ((s2 * p2) `2 )) by Th4

          .= (((1 - s2) * (q `2 )) + (s2 * (p2 `2 ))) by Th4

          .= (p2 `2 ) by A1;

          set t = (((1 - s1) * p2) + (s1 * p3));

          

           A13: (t `1 ) = ((((1 - s1) * p2) `1 ) + ((s1 * p3) `1 )) by Th2

          .= (((1 - s1) * (p2 `1 )) + ((s1 * p3) `1 )) by Th4

          .= (((1 - s1) * (p2 `1 )) + (s1 * (p3 `1 ))) by Th4

          .= (((1 - s1) * (p2 `1 )) + (s1 * (p2 `1 ))) by EUCLID: 52

          .= (p2 `1 );

          t = |[(t `1 ), (t `2 )]| by EUCLID: 53

          .= p2 by A10, A13, A11, A12, EUCLID: 53;

          hence thesis by A10, TARSKI:def 1;

        end;

        let x be object;

        assume x in {p2};

        then

         A14: x = p2 by TARSKI:def 1;

        p2 in l23 & p2 in l by RLTOPSP1: 68;

        hence thesis by A14, XBOOLE_0:def 4;

      end;

      

      thus ((l23 \/ l3) /\ l) = ((l23 /\ l) \/ (l3 /\ l)) by XBOOLE_1: 23

      .= {p2} by A8, A3;

    end;

    theorem :: TOPREAL3:28

    for q, p2, p st (q `1 ) = (p2 `1 ) & (p `1 ) <> (p2 `1 ) holds ((( LSeg (p2, |[(p `1 ), (p2 `2 )]|)) \/ ( LSeg ( |[(p `1 ), (p2 `2 )]|,p))) /\ ( LSeg (q,p2))) = {p2}

    proof

      let q, p2, p such that

       A1: (q `1 ) = (p2 `1 ) and

       A2: (p `1 ) <> (p2 `1 );

      set p3 = |[(p `1 ), (p2 `2 )]|;

      set l23 = ( LSeg (p2,p3)), l3 = ( LSeg (p3,p)), l = ( LSeg (q,p2));

      

       A3: (l3 /\ l) = {}

      proof

        set x = the Element of (l3 /\ l);

        assume

         A4: (l3 /\ l) <> {} ;

        then x in l3 by XBOOLE_0:def 4;

        then

        consider d1 be Real such that

         A5: x = (((1 - d1) * p3) + (d1 * p)) and 0 <= d1 and d1 <= 1;

        x in l by A4, XBOOLE_0:def 4;

        then

        consider d2 be Real such that

         A6: x = (((1 - d2) * q) + (d2 * p2)) and 0 <= d2 and d2 <= 1;

        

         A7: ((((1 - d1) * p3) + (d1 * p)) `1 ) = ((((1 - d1) * p3) `1 ) + ((d1 * p) `1 )) by Th2

        .= (((1 - d1) * (p3 `1 )) + ((d1 * p) `1 )) by Th4

        .= (((1 - d1) * (p3 `1 )) + (d1 * (p `1 ))) by Th4

        .= (((1 - d1) * (p `1 )) + (d1 * (p `1 ))) by EUCLID: 52

        .= (p `1 );

        ((((1 - d2) * q) + (d2 * p2)) `1 ) = ((((1 - d2) * q) `1 ) + ((d2 * p2) `1 )) by Th2

        .= (((1 - d2) * (q `1 )) + ((d2 * p2) `1 )) by Th4

        .= (((1 - d2) * (q `1 )) + (d2 * (p2 `1 ))) by Th4

        .= (p2 `1 ) by A1;

        hence contradiction by A2, A5, A7, A6;

      end;

      

       A8: (l23 /\ l) = {p2}

      proof

        thus (l23 /\ l) c= {p2}

        proof

          let x be object;

          assume

           A9: x in (l23 /\ l);

          then x in l23 by XBOOLE_0:def 4;

          then

          consider s1 be Real such that

           A10: x = (((1 - s1) * p2) + (s1 * p3)) and 0 <= s1 and s1 <= 1;

          x in l by A9, XBOOLE_0:def 4;

          then

          consider s2 be Real such that

           A11: x = (((1 - s2) * q) + (s2 * p2)) and 0 <= s2 and s2 <= 1;

          

           A12: ((((1 - s2) * q) + (s2 * p2)) `1 ) = ((((1 - s2) * q) `1 ) + ((s2 * p2) `1 )) by Th2

          .= (((1 - s2) * (q `1 )) + ((s2 * p2) `1 )) by Th4

          .= (((1 - s2) * (q `1 )) + (s2 * (p2 `1 ))) by Th4

          .= (p2 `1 ) by A1;

          set t = (((1 - s1) * p2) + (s1 * p3));

          

           A13: (t `2 ) = ((((1 - s1) * p2) `2 ) + ((s1 * p3) `2 )) by Th2

          .= (((1 - s1) * (p2 `2 )) + ((s1 * p3) `2 )) by Th4

          .= (((1 - s1) * (p2 `2 )) + (s1 * (p3 `2 ))) by Th4

          .= (((1 - s1) * (p2 `2 )) + (s1 * (p2 `2 ))) by EUCLID: 52

          .= (p2 `2 );

          t = |[(t `1 ), (t `2 )]| by EUCLID: 53

          .= p2 by A10, A13, A11, A12, EUCLID: 53;

          hence thesis by A10, TARSKI:def 1;

        end;

        let x be object;

        assume x in {p2};

        then

         A14: x = p2 by TARSKI:def 1;

        p2 in l23 & p2 in l by RLTOPSP1: 68;

        hence thesis by A14, XBOOLE_0:def 4;

      end;

      

      thus ((l23 \/ l3) /\ l) = ((l23 /\ l) \/ (l3 /\ l)) by XBOOLE_1: 23

      .= {p2} by A8, A3;

    end;

    theorem :: TOPREAL3:29

    

     Th29: (( LSeg (p, |[(p `1 ), (q `2 )]|)) /\ ( LSeg ( |[(p `1 ), (q `2 )]|,q))) = { |[(p `1 ), (q `2 )]|}

    proof

      set p3 = |[(p `1 ), (q `2 )]|;

      set l23 = ( LSeg (p,p3)), l = ( LSeg (p3,q));

      thus (l23 /\ l) c= {p3}

      proof

        let x be object;

        assume

         A1: x in (l23 /\ l);

        then x in l23 by XBOOLE_0:def 4;

        then

        consider d1 be Real such that

         A2: x = (((1 - d1) * p) + (d1 * p3)) and 0 <= d1 and d1 <= 1;

        x in l by A1, XBOOLE_0:def 4;

        then

        consider d2 be Real such that

         A3: x = (((1 - d2) * p3) + (d2 * q)) and 0 <= d2 and d2 <= 1;

        set t = (((1 - d1) * p) + (d1 * p3));

        

         A4: (t `1 ) = ((((1 - d1) * p) `1 ) + ((d1 * p3) `1 )) by Th2

        .= (((1 - d1) * (p `1 )) + ((d1 * p3) `1 )) by Th4

        .= (((1 - d1) * (p `1 )) + (d1 * (p3 `1 ))) by Th4

        .= (((1 - d1) * (p `1 )) + (d1 * (p `1 ))) by EUCLID: 52

        .= (p3 `1 ) by EUCLID: 52;

        (t `2 ) = ((((1 - d2) * p3) `2 ) + ((d2 * q) `2 )) by A2, A3, Th2

        .= (((1 - d2) * (p3 `2 )) + ((d2 * q) `2 )) by Th4

        .= (((1 - d2) * (p3 `2 )) + (d2 * (q `2 ))) by Th4

        .= (((1 - d2) * (q `2 )) + (d2 * (q `2 ))) by EUCLID: 52

        .= (p3 `2 ) by EUCLID: 52;

        then t = p3 by A4, Th6;

        hence thesis by A2, TARSKI:def 1;

      end;

      let x be object;

      assume x in {p3};

      then

       A5: x = p3 by TARSKI:def 1;

      p3 in l23 & p3 in l by RLTOPSP1: 68;

      hence thesis by A5, XBOOLE_0:def 4;

    end;

    theorem :: TOPREAL3:30

    

     Th30: (( LSeg (p, |[(q `1 ), (p `2 )]|)) /\ ( LSeg ( |[(q `1 ), (p `2 )]|,q))) = { |[(q `1 ), (p `2 )]|}

    proof

      set p3 = |[(q `1 ), (p `2 )]|;

      set l23 = ( LSeg (p,p3)), l = ( LSeg (p3,q));

      thus (l23 /\ l) c= {p3}

      proof

        let x be object;

        assume

         A1: x in (l23 /\ l);

        then x in l23 by XBOOLE_0:def 4;

        then

        consider d1 be Real such that

         A2: x = (((1 - d1) * p) + (d1 * p3)) and 0 <= d1 and d1 <= 1;

        x in l by A1, XBOOLE_0:def 4;

        then

        consider d2 be Real such that

         A3: x = (((1 - d2) * p3) + (d2 * q)) and 0 <= d2 and d2 <= 1;

        set t = (((1 - d1) * p) + (d1 * p3));

        

         A4: (t `2 ) = ((((1 - d1) * p) `2 ) + ((d1 * p3) `2 )) by Th2

        .= (((1 - d1) * (p `2 )) + ((d1 * p3) `2 )) by Th4

        .= (((1 - d1) * (p `2 )) + (d1 * (p3 `2 ))) by Th4

        .= (((1 - d1) * (p3 `2 )) + (d1 * (p3 `2 ))) by EUCLID: 52

        .= (p3 `2 );

        (t `1 ) = ((((1 - d2) * p3) `1 ) + ((d2 * q) `1 )) by A2, A3, Th2

        .= (((1 - d2) * (p3 `1 )) + ((d2 * q) `1 )) by Th4

        .= (((1 - d2) * (p3 `1 )) + (d2 * (q `1 ))) by Th4

        .= (((1 - d2) * (p3 `1 )) + (d2 * (p3 `1 ))) by EUCLID: 52

        .= (p3 `1 );

        then t = p3 by A4, Th6;

        hence thesis by A2, TARSKI:def 1;

      end;

      let x be object;

      assume x in {p3};

      then

       A5: x = p3 by TARSKI:def 1;

      p3 in l23 & p3 in l by RLTOPSP1: 68;

      hence thesis by A5, XBOOLE_0:def 4;

    end;

    theorem :: TOPREAL3:31

    

     Th31: (p `1 ) = (q `1 ) & (p `2 ) <> (q `2 ) implies (( LSeg (p, |[(p `1 ), (((p `2 ) + (q `2 )) / 2)]|)) /\ ( LSeg ( |[(p `1 ), (((p `2 ) + (q `2 )) / 2)]|,q))) = { |[(p `1 ), (((p `2 ) + (q `2 )) / 2)]|}

    proof

      assume that

       A1: (p `1 ) = (q `1 ) and

       A2: (p `2 ) <> (q `2 );

      set p3 = |[(p `1 ), (((p `2 ) + (q `2 )) / 2)]|;

      set l23 = ( LSeg (p,p3)), l = ( LSeg (p3,q));

      thus (l23 /\ l) c= {p3}

      proof

        let x be object;

        

         A3: l23 = ( LSeg ( |[(p `1 ), (p `2 )]|, |[(p `1 ), (((p `2 ) + (q `2 )) / 2)]|)) by EUCLID: 53;

        assume

         A4: x in (l23 /\ l);

        then

         A5: x in l by XBOOLE_0:def 4;

        

         A6: l = ( LSeg ( |[(q `1 ), (((p `2 ) + (q `2 )) / 2)]|, |[(q `1 ), (q `2 )]|)) by A1, EUCLID: 53;

        

         A7: x in l23 by A4, XBOOLE_0:def 4;

        now

          per cases by A2, XXREAL_0: 1;

            suppose

             A8: (p `2 ) < (q `2 );

            then (p `2 ) < (((p `2 ) + (q `2 )) / 2) by XREAL_1: 226;

            then x in { p1 : (p1 `1 ) = (p `1 ) & (p `2 ) <= (p1 `2 ) & (p1 `2 ) <= (((p `2 ) + (q `2 )) / 2) } by A7, A3, Th9;

            then

            consider t1 be Point of ( TOP-REAL 2) such that

             A9: t1 = x and

             A10: (t1 `1 ) = (p `1 ) and (p `2 ) <= (t1 `2 ) and

             A11: (t1 `2 ) <= (((p `2 ) + (q `2 )) / 2);

            

             A12: (t1 `2 ) <= (p3 `2 ) by A11, EUCLID: 52;

            (((p `2 ) + (q `2 )) / 2) < (q `2 ) by A8, XREAL_1: 226;

            then x in { p2 : (p2 `1 ) = (q `1 ) & (((p `2 ) + (q `2 )) / 2) <= (p2 `2 ) & (p2 `2 ) <= (q `2 ) } by A5, A6, Th9;

            then ex t2 be Point of ( TOP-REAL 2) st t2 = x & (t2 `1 ) = (q `1 ) & (((p `2 ) + (q `2 )) / 2) <= (t2 `2 ) & (t2 `2 ) <= (q `2 );

            then (t1 `2 ) >= (p3 `2 ) by A9, EUCLID: 52;

            then

             A13: (t1 `2 ) = (p3 `2 ) by A12, XXREAL_0: 1;

            (t1 `1 ) = (p3 `1 ) by A10, EUCLID: 52;

            hence x = p3 by A9, A13, Th6;

          end;

            suppose

             A14: (p `2 ) > (q `2 );

            then (p `2 ) > (((p `2 ) + (q `2 )) / 2) by XREAL_1: 226;

            then x in { p11 : (p11 `1 ) = (p `1 ) & (((p `2 ) + (q `2 )) / 2) <= (p11 `2 ) & (p11 `2 ) <= (p `2 ) } by A7, A3, Th9;

            then

            consider t1 be Point of ( TOP-REAL 2) such that

             A15: t1 = x and

             A16: (t1 `1 ) = (p `1 ) and

             A17: (((p `2 ) + (q `2 )) / 2) <= (t1 `2 ) and (t1 `2 ) <= (p `2 );

            

             A18: (p3 `2 ) <= (t1 `2 ) by A17, EUCLID: 52;

            (q `2 ) < (((p `2 ) + (q `2 )) / 2) by A14, XREAL_1: 226;

            then x in { p22 : (p22 `1 ) = (q `1 ) & (q `2 ) <= (p22 `2 ) & (p22 `2 ) <= (((p `2 ) + (q `2 )) / 2) } by A5, A6, Th9;

            then ex t2 be Point of ( TOP-REAL 2) st t2 = x & (t2 `1 ) = (q `1 ) & (q `2 ) <= (t2 `2 ) & (t2 `2 ) <= (((p `2 ) + (q `2 )) / 2);

            then (t1 `2 ) <= (p3 `2 ) by A15, EUCLID: 52;

            then

             A19: (t1 `2 ) = (p3 `2 ) by A18, XXREAL_0: 1;

            (t1 `1 ) = (p3 `1 ) by A16, EUCLID: 52;

            hence x = p3 by A15, A19, Th6;

          end;

        end;

        hence thesis by TARSKI:def 1;

      end;

      let x be object;

      assume x in {p3};

      then

       A20: x = p3 by TARSKI:def 1;

      p3 in l23 & p3 in l by RLTOPSP1: 68;

      hence thesis by A20, XBOOLE_0:def 4;

    end;

    theorem :: TOPREAL3:32

    

     Th32: (p `1 ) <> (q `1 ) & (p `2 ) = (q `2 ) implies (( LSeg (p, |[(((p `1 ) + (q `1 )) / 2), (p `2 )]|)) /\ ( LSeg ( |[(((p `1 ) + (q `1 )) / 2), (p `2 )]|,q))) = { |[(((p `1 ) + (q `1 )) / 2), (p `2 )]|}

    proof

      assume that

       A1: (p `1 ) <> (q `1 ) and

       A2: (p `2 ) = (q `2 );

      set p3 = |[(((p `1 ) + (q `1 )) / 2), (p `2 )]|;

      set l23 = ( LSeg (p,p3)), l = ( LSeg (p3,q));

      thus (l23 /\ l) c= {p3}

      proof

        let x be object;

        

         A3: l23 = ( LSeg ( |[(p `1 ), (p `2 )]|, |[(((p `1 ) + (q `1 )) / 2), (p `2 )]|)) by EUCLID: 53;

        assume

         A4: x in (l23 /\ l);

        then

         A5: x in l by XBOOLE_0:def 4;

        

         A6: l = ( LSeg ( |[(((p `1 ) + (q `1 )) / 2), (q `2 )]|, |[(q `1 ), (q `2 )]|)) by A2, EUCLID: 53;

        

         A7: x in l23 by A4, XBOOLE_0:def 4;

        now

          per cases by A1, XXREAL_0: 1;

            suppose

             A8: (p `1 ) < (q `1 );

            then (p `1 ) < (((p `1 ) + (q `1 )) / 2) by XREAL_1: 226;

            then x in { p1 : (p1 `2 ) = (p `2 ) & (p `1 ) <= (p1 `1 ) & (p1 `1 ) <= (((p `1 ) + (q `1 )) / 2) } by A7, A3, Th10;

            then

            consider t1 be Point of ( TOP-REAL 2) such that

             A9: t1 = x and

             A10: (t1 `2 ) = (p `2 ) and (p `1 ) <= (t1 `1 ) and

             A11: (t1 `1 ) <= (((p `1 ) + (q `1 )) / 2);

            

             A12: (t1 `1 ) <= (p3 `1 ) by A11, EUCLID: 52;

            (((p `1 ) + (q `1 )) / 2) < (q `1 ) by A8, XREAL_1: 226;

            then x in { p2 : (p2 `2 ) = (q `2 ) & (((p `1 ) + (q `1 )) / 2) <= (p2 `1 ) & (p2 `1 ) <= (q `1 ) } by A5, A6, Th10;

            then ex t2 be Point of ( TOP-REAL 2) st t2 = x & (t2 `2 ) = (q `2 ) & (((p `1 ) + (q `1 )) / 2) <= (t2 `1 ) & (t2 `1 ) <= (q `1 );

            then (t1 `1 ) >= (p3 `1 ) by A9, EUCLID: 52;

            then

             A13: (t1 `1 ) = (p3 `1 ) by A12, XXREAL_0: 1;

            (t1 `2 ) = (p3 `2 ) by A10, EUCLID: 52;

            hence x = p3 by A9, A13, Th6;

          end;

            suppose

             A14: (p `1 ) > (q `1 );

            then (p `1 ) > (((p `1 ) + (q `1 )) / 2) by XREAL_1: 226;

            then x in { p11 : (p11 `2 ) = (p `2 ) & (((p `1 ) + (q `1 )) / 2) <= (p11 `1 ) & (p11 `1 ) <= (p `1 ) } by A7, A3, Th10;

            then

            consider t1 be Point of ( TOP-REAL 2) such that

             A15: t1 = x and

             A16: (t1 `2 ) = (p `2 ) and

             A17: (((p `1 ) + (q `1 )) / 2) <= (t1 `1 ) and (t1 `1 ) <= (p `1 );

            

             A18: (p3 `1 ) <= (t1 `1 ) by A17, EUCLID: 52;

            (q `1 ) < (((p `1 ) + (q `1 )) / 2) by A14, XREAL_1: 226;

            then x in { p22 : (p22 `2 ) = (q `2 ) & (q `1 ) <= (p22 `1 ) & (p22 `1 ) <= (((p `1 ) + (q `1 )) / 2) } by A5, A6, Th10;

            then ex t2 be Point of ( TOP-REAL 2) st t2 = x & (t2 `2 ) = (q `2 ) & (q `1 ) <= (t2 `1 ) & (t2 `1 ) <= (((p `1 ) + (q `1 )) / 2);

            then (t1 `1 ) <= (p3 `1 ) by A15, EUCLID: 52;

            then

             A19: (t1 `1 ) = (p3 `1 ) by A18, XXREAL_0: 1;

            (t1 `2 ) = (p3 `2 ) by A16, EUCLID: 52;

            hence x = p3 by A15, A19, Th6;

          end;

        end;

        hence thesis by TARSKI:def 1;

      end;

      let x be object;

      assume x in {p3};

      then

       A20: x = p3 by TARSKI:def 1;

      p3 in l23 & p3 in l by RLTOPSP1: 68;

      hence thesis by A20, XBOOLE_0:def 4;

    end;

    theorem :: TOPREAL3:33

    i > 2 & i in ( dom f) & f is being_S-Seq implies (f | i) is being_S-Seq

    proof

      assume that

       A1: i > 2 and

       A2: i in ( dom f) and

       A3: f is being_S-Seq;

      

       A4: (f | i) = (f | ( Seg i)) by FINSEQ_1:def 15;

      then

       A5: ( dom (f | i)) = (( dom f) /\ ( Seg i)) by RELAT_1: 61;

      thus (f | i) is one-to-one

      proof

        

         A6: f is one-to-one by A3;

        let x,y be object;

        assume that

         A7: x in ( dom (f | i)) and

         A8: y in ( dom (f | i)) and

         A9: ((f | i) . x) = ((f | i) . y);

        

         A10: x in ( dom f) & y in ( dom f) by A5, A7, A8, XBOOLE_0:def 4;

        (f . x) = ((f | i) . x) by A4, A7, FUNCT_1: 47

        .= (f . y) by A4, A8, A9, FUNCT_1: 47;

        hence thesis by A6, A10;

      end;

      

       A11: i <= ( len f) by A2, FINSEQ_3: 25;

      

       A12: i in NAT by ORDINAL1:def 12;

      ( Seg ( len f)) = ( dom f) by FINSEQ_1:def 3;

      then ( Seg i) c= ( dom f) by A11, FINSEQ_1: 5;

      then

       A13: ( dom (f | i)) = ( Seg i) by A5, XBOOLE_1: 28;

      hence ( len (f | i)) >= 2 by A1, A12, FINSEQ_1:def 3;

      

       A14: f is unfolded by A3;

      thus (f | i) is unfolded

      proof

        let j be Nat such that

         A15: 1 <= j and

         A16: (j + 2) <= ( len (f | i));

        (j + 1) <= (j + 2) by XREAL_1: 6;

        then

         A17: (j + 1) <= ( len (f | i)) by A16, XXREAL_0: 2;

        ( len (f | i)) <= ( len f) by A11, A13, A12, FINSEQ_1:def 3;

        then

         A18: (j + 2) <= ( len f) by A16, XXREAL_0: 2;

        1 <= (j + 1) by NAT_1: 12;

        then

         A19: (j + 1) in ( dom (f | i)) by A17, FINSEQ_3: 25;

        1 <= ((j + 1) + 1) by NAT_1: 12;

        then ((j + 1) + 1) in ( dom (f | i)) by A16, FINSEQ_3: 25;

        then

         A20: ( LSeg (f,(j + 1))) = ( LSeg ((f | i),(j + 1))) by A19, Th17;

        j <= (j + 2) by NAT_1: 11;

        then j <= ( len (f | i)) by A16, XXREAL_0: 2;

        then j in ( dom (f | i)) by A15, FINSEQ_3: 25;

        then ( LSeg (f,j)) = ( LSeg ((f | i),j)) by A19, Th17;

        then (( LSeg ((f | i),j)) /\ ( LSeg ((f | i),(j + 1)))) = {(f /. (j + 1))} by A14, A15, A18, A20;

        hence thesis by A19, FINSEQ_4: 70;

      end;

      

       A21: f is s.n.c. by A3;

      thus (f | i) is s.n.c.

      proof

        let n,k be Nat;

        

         A22: (k + 1) >= 1 by NAT_1: 11;

        

         A23: (n + 1) >= 1 by NAT_1: 11;

        assume (n + 1) < k;

        then ( LSeg (f,n)) misses ( LSeg (f,k)) by A21;

        then

         A24: (( LSeg (f,n)) /\ ( LSeg (f,k))) = {} ;

        

         A25: (k + 1) >= k by NAT_1: 11;

        

         A26: (n + 1) >= n by NAT_1: 11;

        per cases ;

          suppose

           A27: n in ( dom (f | i));

          now

            per cases ;

              suppose (n + 1) in ( dom (f | i));

              then

               A28: ( LSeg (f,n)) = ( LSeg ((f | i),n)) by A27, Th17;

              now

                per cases ;

                  suppose

                   A29: k in ( dom (f | i));

                  now

                    per cases ;

                      suppose (k + 1) in ( dom (f | i));

                      hence (( LSeg ((f | i),n)) /\ ( LSeg ((f | i),k))) = {} by A24, A28, A29, Th17;

                    end;

                      suppose not (k + 1) in ( dom (f | i));

                      then (k + 1) > ( len (f | i)) by A22, FINSEQ_3: 25;

                      then ( LSeg ((f | i),k)) = {} by TOPREAL1:def 3;

                      hence (( LSeg ((f | i),n)) /\ ( LSeg ((f | i),k))) = {} ;

                    end;

                  end;

                  hence (( LSeg ((f | i),n)) /\ ( LSeg ((f | i),k))) = {} ;

                end;

                  suppose not k in ( dom (f | i));

                  then k < 1 or k > ( len (f | i)) by FINSEQ_3: 25;

                  then k < 1 or (k + 1) > ( len (f | i)) by A25, XXREAL_0: 2;

                  then ( LSeg ((f | i),k)) = {} by TOPREAL1:def 3;

                  hence (( LSeg ((f | i),n)) /\ ( LSeg ((f | i),k))) = {} ;

                end;

              end;

              hence (( LSeg ((f | i),n)) /\ ( LSeg ((f | i),k))) = {} ;

            end;

              suppose not (n + 1) in ( dom (f | i));

              then (n + 1) > ( len (f | i)) by A23, FINSEQ_3: 25;

              then ( LSeg ((f | i),n)) = {} by TOPREAL1:def 3;

              hence (( LSeg ((f | i),n)) /\ ( LSeg ((f | i),k))) = {} ;

            end;

          end;

          hence (( LSeg ((f | i),n)) /\ ( LSeg ((f | i),k))) = {} ;

        end;

          suppose not n in ( dom (f | i));

          then n < 1 or n > ( len (f | i)) by FINSEQ_3: 25;

          then n < 1 or (n + 1) > ( len (f | i)) by A26, XXREAL_0: 2;

          then ( LSeg ((f | i),n)) = {} by TOPREAL1:def 3;

          hence (( LSeg ((f | i),n)) /\ ( LSeg ((f | i),k))) = {} ;

        end;

      end;

      let j be Nat such that

       A30: 1 <= j and

       A31: (j + 1) <= ( len (f | i));

      ( len (f | i)) <= ( len f) by A11, A13, A12, FINSEQ_1:def 3;

      then

       A32: (j + 1) <= ( len f) by A31, XXREAL_0: 2;

      j <= (j + 1) by NAT_1: 11;

      then j <= ( len (f | i)) by A31, XXREAL_0: 2;

      then j in ( dom (f | i)) by A30, FINSEQ_3: 25;

      then

       A33: ((f | i) /. j) = (f /. j) by FINSEQ_4: 70;

      1 <= (j + 1) by NAT_1: 12;

      then (j + 1) in ( dom (f | i)) by A31, FINSEQ_3: 25;

      then

       A34: ((f | i) /. (j + 1)) = (f /. (j + 1)) by FINSEQ_4: 70;

      f is special by A3;

      hence thesis by A30, A32, A33, A34;

    end;

    theorem :: TOPREAL3:34

    (p `1 ) <> (q `1 ) & (p `2 ) <> (q `2 ) & f = <*p, |[(p `1 ), (q `2 )]|, q*> implies (f /. 1) = p & (f /. ( len f)) = q & f is being_S-Seq

    proof

      set p1 = |[(p `1 ), (q `2 )]|;

      assume that

       A1: (p `1 ) <> (q `1 ) and

       A2: (p `2 ) <> (q `2 ) and

       A3: f = <*p, p1, q*>;

      

       A4: ( len f) = (1 + 2) by A3, FINSEQ_1: 45;

      hence (f /. 1) = p & (f /. ( len f)) = q by A3, FINSEQ_4: 18;

      p <> p1 & q <> p1 by A1, A2, EUCLID: 52;

      hence f is one-to-one & ( len f) >= 2 by A1, A3, A4, FINSEQ_3: 95;

      

       A5: (f /. 2) = p1 by A3, FINSEQ_4: 18;

      

       A6: (f /. 3) = q by A3, FINSEQ_4: 18;

      

       A7: (f /. 1) = p by A3, FINSEQ_4: 18;

      thus f is unfolded

      proof

        let i be Nat;

        assume that

         A8: 1 <= i and

         A9: (i + 2) <= ( len f);

        i <= 1 by A4, A9, XREAL_1: 6;

        then

         A10: i = 1 by A8, XXREAL_0: 1;

        

        hence (( LSeg (f,i)) /\ ( LSeg (f,(i + 1)))) = (( LSeg (p,p1)) /\ ( LSeg (f,2))) by A4, A7, A5, TOPREAL1:def 3

        .= (( LSeg (p,p1)) /\ ( LSeg (p1,q))) by A4, A5, A6, TOPREAL1:def 3

        .= {(f /. (i + 1))} by A5, A10, Th29;

      end;

      thus f is s.n.c.

      proof

        let i,j be Nat such that

         A11: (i + 1) < j;

        now

          per cases ;

            suppose i = 0 ;

            then ( LSeg (f,i)) = {} by TOPREAL1:def 3;

            then (( LSeg (f,i)) /\ ( LSeg (f,j))) = {} ;

            hence thesis;

          end;

            suppose i <> 0 ;

            then ( LSeg (f,j)) = {} by A3, A11, Th15;

            then (( LSeg (f,i)) /\ ( LSeg (f,j))) = {} ;

            hence thesis;

          end;

        end;

        hence thesis;

      end;

      let i be Nat such that

       A12: 1 <= i and

       A13: (i + 1) <= ( len f);

      i <= 2 by A4, A13, XREAL_1: 6;

      then i = 0 or ... or i = 2;

      per cases by A12;

        suppose i = 1;

        hence thesis by A7, A5, EUCLID: 52;

      end;

        suppose i = 2;

        hence thesis by A5, A6, EUCLID: 52;

      end;

    end;

    theorem :: TOPREAL3:35

    (p `1 ) <> (q `1 ) & (p `2 ) <> (q `2 ) & f = <*p, |[(q `1 ), (p `2 )]|, q*> implies (f /. 1) = p & (f /. ( len f)) = q & f is being_S-Seq

    proof

      set p1 = |[(q `1 ), (p `2 )]|;

      assume that

       A1: (p `1 ) <> (q `1 ) and

       A2: (p `2 ) <> (q `2 ) and

       A3: f = <*p, p1, q*>;

      

       A4: ( len f) = (1 + 2) by A3, FINSEQ_1: 45;

      hence (f /. 1) = p & (f /. ( len f)) = q by A3, FINSEQ_4: 18;

      p <> p1 & q <> p1 by A1, A2, EUCLID: 52;

      hence f is one-to-one & ( len f) >= 2 by A1, A3, A4, FINSEQ_3: 95;

      

       A5: (f /. 2) = p1 by A3, FINSEQ_4: 18;

      

       A6: (f /. 3) = q by A3, FINSEQ_4: 18;

      

       A7: (f /. 1) = p by A3, FINSEQ_4: 18;

      thus f is unfolded

      proof

        let i be Nat;

        assume that

         A8: 1 <= i and

         A9: (i + 2) <= ( len f);

        i <= 1 by A4, A9, XREAL_1: 6;

        then

         A10: i = 1 by A8, XXREAL_0: 1;

        

        hence (( LSeg (f,i)) /\ ( LSeg (f,(i + 1)))) = (( LSeg (p,p1)) /\ ( LSeg (f,2))) by A4, A7, A5, TOPREAL1:def 3

        .= (( LSeg (p,p1)) /\ ( LSeg (p1,q))) by A4, A5, A6, TOPREAL1:def 3

        .= {(f /. (i + 1))} by A5, A10, Th30;

      end;

      thus f is s.n.c.

      proof

        let i,j be Nat such that

         A11: (i + 1) < j;

        now

          per cases ;

            suppose i = 0 ;

            then ( LSeg (f,i)) = {} by TOPREAL1:def 3;

            then (( LSeg (f,i)) /\ ( LSeg (f,j))) = {} ;

            hence thesis;

          end;

            suppose i <> 0 ;

            then ( LSeg (f,j)) = {} by A3, A11, Th15;

            then (( LSeg (f,i)) /\ ( LSeg (f,j))) = {} ;

            hence thesis;

          end;

        end;

        hence thesis;

      end;

      let i be Nat such that

       A12: 1 <= i and

       A13: (i + 1) <= ( len f);

      i <= 2 by A4, A13, XREAL_1: 6;

      then i = 0 or ... or i = 2;

      per cases by A12;

        suppose i = 1;

        hence thesis by A7, A5, EUCLID: 52;

      end;

        suppose i = 2;

        hence thesis by A5, A6, EUCLID: 52;

      end;

    end;

    theorem :: TOPREAL3:36

    (p `1 ) = (q `1 ) & (p `2 ) <> (q `2 ) & f = <*p, |[(p `1 ), (((p `2 ) + (q `2 )) / 2)]|, q*> implies (f /. 1) = p & (f /. ( len f)) = q & f is being_S-Seq

    proof

      set p1 = |[(p `1 ), (((p `2 ) + (q `2 )) / 2)]|;

      assume that

       A1: (p `1 ) = (q `1 ) and

       A2: (p `2 ) <> (q `2 ) and

       A3: f = <*p, p1, q*>;

      

       A4: (p1 `2 ) = (((p `2 ) + (q `2 )) / 2) by EUCLID: 52;

      

       A5: ( len f) = (1 + 2) by A3, FINSEQ_1: 45;

      hence (f /. 1) = p & (f /. ( len f)) = q by A3, FINSEQ_4: 18;

      (p `2 ) <> (((p `2 ) + (q `2 )) / 2) & (q `2 ) <> (((p `2 ) + (q `2 )) / 2) by A2;

      hence f is one-to-one & ( len f) >= 2 by A2, A3, A5, A4, FINSEQ_3: 95;

      

       A6: (f /. 2) = p1 by A3, FINSEQ_4: 18;

      

       A7: (f /. 3) = q by A3, FINSEQ_4: 18;

      

       A8: (f /. 1) = p by A3, FINSEQ_4: 18;

      thus f is unfolded

      proof

        let i be Nat;

        assume that

         A9: 1 <= i and

         A10: (i + 2) <= ( len f);

        i <= 1 by A5, A10, XREAL_1: 6;

        then

         A11: i = 1 by A9, XXREAL_0: 1;

        

        hence (( LSeg (f,i)) /\ ( LSeg (f,(i + 1)))) = (( LSeg (p,p1)) /\ ( LSeg (f,2))) by A5, A8, A6, TOPREAL1:def 3

        .= (( LSeg (p,p1)) /\ ( LSeg (p1,q))) by A5, A6, A7, TOPREAL1:def 3

        .= {(f /. (i + 1))} by A1, A2, A6, A11, Th31;

      end;

      thus f is s.n.c.

      proof

        let i,j be Nat such that

         A12: (i + 1) < j;

        now

          per cases ;

            suppose i = 0 ;

            then ( LSeg (f,i)) = {} by TOPREAL1:def 3;

            then (( LSeg (f,i)) /\ ( LSeg (f,j))) = {} ;

            hence thesis;

          end;

            suppose i <> 0 ;

            then ( LSeg (f,j)) = {} by A3, A12, Th15;

            then (( LSeg (f,i)) /\ ( LSeg (f,j))) = {} ;

            hence thesis;

          end;

        end;

        hence thesis;

      end;

      let i be Nat such that

       A13: 1 <= i and

       A14: (i + 1) <= ( len f);

      i <= 2 by A5, A14, XREAL_1: 6;

      then i = 0 or ... or i = 2;

      per cases by A13;

        suppose i = 1;

        hence thesis by A8, A6, EUCLID: 52;

      end;

        suppose i = 2;

        hence thesis by A1, A6, A7, EUCLID: 52;

      end;

    end;

    theorem :: TOPREAL3:37

    (p `1 ) <> (q `1 ) & (p `2 ) = (q `2 ) & f = <*p, |[(((p `1 ) + (q `1 )) / 2), (p `2 )]|, q*> implies (f /. 1) = p & (f /. ( len f)) = q & f is being_S-Seq

    proof

      set p1 = |[(((p `1 ) + (q `1 )) / 2), (p `2 )]|;

      assume that

       A1: (p `1 ) <> (q `1 ) and

       A2: (p `2 ) = (q `2 ) and

       A3: f = <*p, p1, q*>;

      

       A4: (p1 `1 ) = (((p `1 ) + (q `1 )) / 2) by EUCLID: 52;

      

       A5: ( len f) = (1 + 2) by A3, FINSEQ_1: 45;

      hence (f /. 1) = p & (f /. ( len f)) = q by A3, FINSEQ_4: 18;

      (p `1 ) <> (((p `1 ) + (q `1 )) / 2) & (q `1 ) <> (((p `1 ) + (q `1 )) / 2) by A1;

      hence f is one-to-one & ( len f) >= 2 by A1, A3, A5, A4, FINSEQ_3: 95;

      

       A6: (f /. 2) = p1 by A3, FINSEQ_4: 18;

      

       A7: (f /. 3) = q by A3, FINSEQ_4: 18;

      

       A8: (f /. 1) = p by A3, FINSEQ_4: 18;

      thus f is unfolded

      proof

        let i be Nat;

        assume that

         A9: 1 <= i and

         A10: (i + 2) <= ( len f);

        i <= 1 by A5, A10, XREAL_1: 6;

        then

         A11: i = 1 by A9, XXREAL_0: 1;

        

        hence (( LSeg (f,i)) /\ ( LSeg (f,(i + 1)))) = (( LSeg (p,p1)) /\ ( LSeg (f,2))) by A5, A8, A6, TOPREAL1:def 3

        .= (( LSeg (p,p1)) /\ ( LSeg (p1,q))) by A5, A6, A7, TOPREAL1:def 3

        .= {(f /. (i + 1))} by A1, A2, A6, A11, Th32;

      end;

      thus f is s.n.c.

      proof

        let i,j be Nat such that

         A12: (i + 1) < j;

        now

          per cases ;

            suppose i = 0 ;

            then ( LSeg (f,i)) = {} by TOPREAL1:def 3;

            then (( LSeg (f,i)) /\ ( LSeg (f,j))) = {} ;

            hence thesis;

          end;

            suppose i <> 0 ;

            then ( LSeg (f,j)) = {} by A3, A12, Th15;

            then (( LSeg (f,i)) /\ ( LSeg (f,j))) = {} ;

            hence thesis;

          end;

        end;

        hence thesis;

      end;

      let i be Nat such that

       A13: 1 <= i and

       A14: (i + 1) <= ( len f);

      i <= 2 by A5, A14, XREAL_1: 6;

      then i = 0 or ... or i = 2;

      per cases by A13;

        suppose i = 1;

        hence thesis by A8, A6, EUCLID: 52;

      end;

        suppose i = 2;

        hence thesis by A2, A6, A7, EUCLID: 52;

      end;

    end;

    theorem :: TOPREAL3:38

    i in ( dom f) & (i + 1) in ( dom f) implies ( L~ (f | (i + 1))) = (( L~ (f | i)) \/ ( LSeg ((f /. i),(f /. (i + 1)))))

    proof

      set M1 = { ( LSeg ((f | (i + 1)),k)) : 1 <= k & (k + 1) <= ( len (f | (i + 1))) }, Mi = { ( LSeg ((f | i),n)) : 1 <= n & (n + 1) <= ( len (f | i)) };

      assume that

       A1: i in ( dom f) and

       A2: (i + 1) in ( dom f);

      set p = (f /. i), q = (f /. (i + 1));

      

       A3: (i + 1) <= ( len f) by A2, FINSEQ_3: 25;

      then ( Seg (i + 1)) c= ( Seg ( len f)) by FINSEQ_1: 5;

      then ( Seg (i + 1)) c= ( dom f) by FINSEQ_1:def 3;

      then ( Seg (i + 1)) = (( dom f) /\ ( Seg (i + 1))) by XBOOLE_1: 28;

      then

       A4: (f | (i + 1)) = (f | ( Seg (i + 1))) & ( Seg (i + 1)) = ( dom (f | ( Seg (i + 1)))) by FINSEQ_1:def 15, RELAT_1: 61;

      then

       A5: (i + 1) = ( len (f | (i + 1))) by FINSEQ_1:def 3;

      

       A6: 1 <= i by A1, FINSEQ_3: 25;

      then

       A7: ( LSeg (f,i)) = ( LSeg (p,q)) by A3, TOPREAL1:def 3;

      1 <= (i + 1) by A2, FINSEQ_3: 25;

      then

       A8: (i + 1) in ( dom (f | (i + 1))) by A5, FINSEQ_3: 25;

      

       A9: i <= (i + 1) by NAT_1: 11;

      then i in ( dom (f | (i + 1))) by A6, A5, FINSEQ_3: 25;

      then

       A10: ( LSeg ((f | (i + 1)),i)) = ( LSeg (p,q)) by A7, A8, Th17;

      then

       A11: ( LSeg (p,q)) c= ( L~ (f | (i + 1))) by Th19;

      

       A12: i in NAT by ORDINAL1:def 12;

      i <= ( len f) by A1, FINSEQ_3: 25;

      then ( Seg i) c= ( Seg ( len f)) by FINSEQ_1: 5;

      then ( Seg i) c= ( dom f) by FINSEQ_1:def 3;

      then (( dom f) /\ ( Seg i)) = ( Seg i) by XBOOLE_1: 28;

      then

       A13: (f | i) = (f | ( Seg i)) & ( dom (f | ( Seg i))) = ( Seg i) by FINSEQ_1:def 15, RELAT_1: 61;

      then

       A14: i = ( len (f | i)) by A12, FINSEQ_1:def 3;

      

       A15: ( Seg ( len (f | (i + 1)))) = ( dom (f | (i + 1))) by FINSEQ_1:def 3;

      thus ( L~ (f | (i + 1))) c= (( L~ (f | i)) \/ ( LSeg (p,q)))

      proof

        let x be object;

        assume x in ( L~ (f | (i + 1)));

        then

        consider X be set such that

         A16: x in X and

         A17: X in M1 by TARSKI:def 4;

        consider m such that

         A18: X = ( LSeg ((f | (i + 1)),m)) and

         A19: 1 <= m and

         A20: (m + 1) <= ( len (f | (i + 1))) by A17;

        

         A21: m <= i by A5, A20, XREAL_1: 6;

        per cases by A21, XXREAL_0: 1;

          suppose m = i;

          then X c= (( L~ (f | i)) \/ ( LSeg (p,q))) by A10, A18, XBOOLE_1: 7;

          hence thesis by A16;

        end;

          suppose

           A22: m < i;

          then m <= (i + 1) by NAT_1: 13;

          then

           A23: m in ( dom (f | (i + 1))) by A4, A19, FINSEQ_1: 1;

          

           A24: m in ( dom (f | i)) by A13, A19, A22, FINSEQ_1: 1;

          

           A25: 1 <= (m + 1) by A19, NAT_1: 13;

          

           A26: (m + 1) <= i by A22, NAT_1: 13;

          then

           A27: (m + 1) in ( dom (f | i)) by A13, A25, FINSEQ_1: 1;

          (m + 1) in ( dom (f | (i + 1))) by A15, A20, A25, FINSEQ_1: 1;

          

          then X = ( LSeg (f,m)) by A18, A23, Th17

          .= ( LSeg ((f | i),m)) by A24, A27, Th17;

          then X in Mi by A14, A19, A26;

          then x in ( union Mi) by A16, TARSKI:def 4;

          hence thesis by XBOOLE_0:def 3;

        end;

      end;

      let x be object such that

       A28: x in (( L~ (f | i)) \/ ( LSeg (p,q)));

      per cases by A28, XBOOLE_0:def 3;

        suppose x in ( L~ (f | i));

        then

        consider X be set such that

         A29: x in X and

         A30: X in Mi by TARSKI:def 4;

        consider m such that

         A31: X = ( LSeg ((f | i),m)) and

         A32: 1 <= m and

         A33: (m + 1) <= ( len (f | i)) by A30;

        

         A34: 1 <= (m + 1) by NAT_1: 11;

        then

         A35: (m + 1) in ( dom (f | i)) by A33, FINSEQ_3: 25;

        m <= (m + 1) by NAT_1: 11;

        then

         A36: m <= ( len (f | i)) by A33, XXREAL_0: 2;

        then m <= ( len (f | (i + 1))) by A5, A14, A9, XXREAL_0: 2;

        then

         A37: m in ( dom (f | (i + 1))) by A32, FINSEQ_3: 25;

        

         A38: (m + 1) <= ( len (f | (i + 1))) by A5, A14, A9, A33, XXREAL_0: 2;

        then

         A39: (m + 1) in ( dom (f | (i + 1))) by A34, FINSEQ_3: 25;

        m in ( dom (f | i)) by A32, A36, FINSEQ_3: 25;

        

        then X = ( LSeg (f,m)) by A31, A35, Th17

        .= ( LSeg ((f | (i + 1)),m)) by A37, A39, Th17;

        then X in M1 by A32, A38;

        hence thesis by A29, TARSKI:def 4;

      end;

        suppose x in ( LSeg (p,q));

        hence thesis by A11;

      end;

    end;

    theorem :: TOPREAL3:39

    ( len f) >= 2 & not p in ( L~ f) implies for n st 1 <= n & n <= ( len f) holds (f /. n) <> p

    proof

      assume that

       A1: ( len f) >= 2 and

       A2: not p in ( L~ f);

      set Mf = { ( LSeg (f,k)) : 1 <= k & (k + 1) <= ( len f) };

      given n such that

       A3: 1 <= n and

       A4: n <= ( len f) and

       A5: (f /. n) = p;

      per cases by A4, XXREAL_0: 1;

        suppose

         A6: n = ( len f);

        reconsider j = (( len f) - 1) as Element of NAT by A1, INT_1: 5, XXREAL_0: 2;

        (1 + 1) <= ( len f) by A1;

        then

         A7: 1 <= j by XREAL_1: 19;

        then

         A8: (f /. (j + 1)) in ( LSeg (f,j)) by TOPREAL1: 21;

        (j + 1) <= ( len f);

        then ( LSeg (f,j)) in Mf by A7;

        hence contradiction by A2, A5, A6, A8, TARSKI:def 4;

      end;

        suppose

         A9: n < ( len f);

        then (n + 1) <= ( len f) by NAT_1: 13;

        then

         A10: (f /. n) in ( LSeg (f,n)) by A3, TOPREAL1: 21;

        (n + 1) <= ( len f) by A9, NAT_1: 13;

        then ( LSeg (f,n)) in Mf by A3;

        hence contradiction by A2, A5, A10, TARSKI:def 4;

      end;

    end;

    theorem :: TOPREAL3:40

    q <> p & (( LSeg (q,p)) /\ ( L~ f)) = {q} implies not p in ( L~ f)

    proof

      assume that

       A1: q <> p and

       A2: (( LSeg (q,p)) /\ ( L~ f)) = {q} & p in ( L~ f);

      p in ( LSeg (q,p)) by RLTOPSP1: 68;

      then p in {q} by A2, XBOOLE_0:def 4;

      hence contradiction by A1, TARSKI:def 1;

    end;

    theorem :: TOPREAL3:41

    f is being_S-Seq & (f /. ( len f)) in ( LSeg (f,m)) & 1 <= m & (m + 1) <= ( len f) implies (m + 1) = ( len f)

    proof

      assume that

       A1: f is being_S-Seq and

       A2: (f /. ( len f)) in ( LSeg (f,m)) and

       A3: 1 <= m and

       A4: (m + 1) <= ( len f);

      

       A5: f is s.n.c. by A1;

      

       A6: f is one-to-one by A1;

      

       A7: f is unfolded by A1;

      set q = (f /. ( len f));

      

       A8: ((m + 1) + 1) = (m + (1 + 1));

      

       A9: ( len f) >= 2 by A1;

      then

      reconsider k = (( len f) - 1) as Element of NAT by INT_1: 5, XXREAL_0: 2;

      

       A10: (k + 1) = ( len f);

      assume (m + 1) <> ( len f);

      then

       A11: (m + 1) <= k by A4, A10, NAT_1: 8;

      1 <= ( len f) by A9, XXREAL_0: 2;

      then

       A12: ( len f) in ( dom f) by FINSEQ_3: 25;

      per cases by A11, XXREAL_0: 1;

        suppose

         A13: (m + 1) = k;

        

         A14: 1 <= (m + 1) by NAT_1: 11;

        ((m + 1) + 1) <= ( len f) by A13;

        then

         A15: (f /. (m + 2)) in ( LSeg (f,(m + 1))) by A14, TOPREAL1: 21;

        (( LSeg (f,m)) /\ ( LSeg (f,(m + 1)))) = {(f /. (m + 1))} by A3, A7, A8, A13;

        then q in {(f /. (m + 1))} by A2, A13, A15, XBOOLE_0:def 4;

        then

         A16: (f /. ( len f)) = (f /. (m + 1)) by TARSKI:def 1;

        (m + 1) <= ( len f) by A10, A13, NAT_1: 11;

        then (m + 1) in ( dom f) by A14, FINSEQ_3: 25;

        then ( len f) = (( len f) - 1) by A6, A12, A13, A16, PARTFUN2: 10;

        hence contradiction;

      end;

        suppose

         A17: (m + 1) < k;

        ((1 + 1) - 1) = 1;

        then (k + 1) = ( len f) & 1 <= k by A9, XREAL_1: 13;

        then

         A18: q in ( LSeg (f,k)) by TOPREAL1: 21;

        ( LSeg (f,m)) misses ( LSeg (f,k)) by A5, A17;

        then (( LSeg (f,m)) /\ ( LSeg (f,k))) = {} ;

        hence contradiction by A2, A18, XBOOLE_0:def 4;

      end;

    end;

    theorem :: TOPREAL3:42

     not p1 in ( Ball (u,r)) & q in ( Ball (u,r)) & p in ( Ball (u,r)) & not p in ( LSeg (p1,q)) & ((q `1 ) = (p `1 ) & (q `2 ) <> (p `2 ) or (q `1 ) <> (p `1 ) & (q `2 ) = (p `2 )) & ((p1 `1 ) = (q `1 ) or (p1 `2 ) = (q `2 )) implies (( LSeg (p1,q)) /\ ( LSeg (q,p))) = {q}

    proof

      assume that

       A1: not p1 in ( Ball (u,r)) and

       A2: q in ( Ball (u,r)) and

       A3: p in ( Ball (u,r)) and

       A4: not p in ( LSeg (p1,q));

      assume

       A5: (q `1 ) = (p `1 ) & (q `2 ) <> (p `2 ) or (q `1 ) <> (p `1 ) & (q `2 ) = (p `2 );

      assume

       A6: (p1 `1 ) = (q `1 ) or (p1 `2 ) = (q `2 );

       A7:

      now

        per cases by A6;

          suppose (p1 `1 ) = (q `1 );

          hence (p1 `1 ) = (q `1 ) & (p1 `2 ) <> (q `2 ) or (p1 `1 ) <> (q `1 ) & (p1 `2 ) = (q `2 ) by A1, A2, Th6;

        end;

          suppose (p1 `2 ) = (q `2 );

          hence (p1 `1 ) = (q `1 ) & (p1 `2 ) <> (q `2 ) or (p1 `1 ) <> (q `1 ) & (p1 `2 ) = (q `2 ) by A1, A2, Th6;

        end;

      end;

      

       A8: p = |[(p `1 ), (p `2 )]| by EUCLID: 53;

      

       A9: p1 = |[(p1 `1 ), (p1 `2 )]| by EUCLID: 53;

      

       A10: q = |[(q `1 ), (q `2 )]| by EUCLID: 53;

      

       A11: ( LSeg (p,q)) c= ( Ball (u,r)) by A2, A3, Th21;

      now

        per cases by A5;

          suppose

           A12: (q `1 ) = (p `1 ) & (q `2 ) <> (p `2 );

          set r = (p `1 ), pq = { p2 : (p2 `1 ) = r & (p `2 ) <= (p2 `2 ) & (p2 `2 ) <= (q `2 ) }, qp = { p3 : (p3 `1 ) = r & (q `2 ) <= (p3 `2 ) & (p3 `2 ) <= (p `2 ) }, pp1 = { p11 : (p11 `1 ) = r & (p `2 ) <= (p11 `2 ) & (p11 `2 ) <= (p1 `2 ) }, p1p = { p22 : (p22 `1 ) = r & (p1 `2 ) <= (p22 `2 ) & (p22 `2 ) <= (p `2 ) }, qp1 = { q1 : (q1 `1 ) = r & (q `2 ) <= (q1 `2 ) & (q1 `2 ) <= (p1 `2 ) }, p1q = { q2 : (q2 `1 ) = r & (p1 `2 ) <= (q2 `2 ) & (q2 `2 ) <= (q `2 ) };

          now

            per cases by A12, XXREAL_0: 1;

              suppose

               A13: (q `2 ) > (p `2 );

              now

                per cases by A7;

                  suppose

                   A14: (p1 `1 ) = (q `1 ) & (p1 `2 ) <> (q `2 );

                  now

                    per cases by A14, XXREAL_0: 1;

                      case

                       A15: (p1 `2 ) > (q `2 );

                      then q in pp1 by A12, A13;

                      then q in ( LSeg (p,p1)) by A8, A9, A12, A13, A14, A15, Th9, XXREAL_0: 2;

                      hence thesis by TOPREAL1: 8;

                    end;

                      case

                       A16: (p1 `2 ) < (q `2 );

                      now

                        per cases by XXREAL_0: 1;

                          suppose

                           A17: (p1 `2 ) > (p `2 );

                          then p1 in pq by A12, A14, A16;

                          then p1 in ( LSeg (p,q)) by A8, A10, A12, A16, A17, Th9, XXREAL_0: 2;

                          hence contradiction by A1, A11;

                        end;

                          suppose (p1 `2 ) = (p `2 );

                          hence contradiction by A1, A3, A12, A14, Th6;

                        end;

                          suppose (p1 `2 ) < (p `2 );

                          then p in p1q by A13;

                          hence contradiction by A4, A9, A10, A12, A14, A16, Th9;

                        end;

                      end;

                      hence contradiction;

                    end;

                  end;

                  hence thesis;

                end;

                  suppose (p1 `1 ) <> (q `1 ) & (p1 `2 ) = (q `2 );

                  hence thesis by A10, A12, Th30;

                end;

              end;

              hence thesis;

            end;

              suppose

               A18: (q `2 ) < (p `2 );

              now

                per cases by A7;

                  suppose

                   A19: (p1 `1 ) = (q `1 ) & (p1 `2 ) <> (q `2 );

                  now

                    per cases by A19, XXREAL_0: 1;

                      case

                       A20: (p1 `2 ) > (q `2 );

                      now

                        per cases by XXREAL_0: 1;

                          suppose (p1 `2 ) > (p `2 );

                          then p in qp1 by A18;

                          hence contradiction by A4, A9, A10, A12, A19, A20, Th9;

                        end;

                          suppose (p1 `2 ) = (p `2 );

                          hence contradiction by A1, A3, A12, A19, Th6;

                        end;

                          suppose (p1 `2 ) < (p `2 );

                          then p1 in qp by A12, A19, A20;

                          then p1 in ( LSeg (p,q)) by A8, A10, A12, A18, Th9;

                          hence contradiction by A1, A11;

                        end;

                      end;

                      hence contradiction;

                    end;

                      case

                       A21: (p1 `2 ) < (q `2 );

                      then q in p1p by A12, A18;

                      then q in ( LSeg (p1,p)) by A8, A9, A12, A18, A19, A21, Th9, XXREAL_0: 2;

                      hence thesis by TOPREAL1: 8;

                    end;

                  end;

                  hence thesis;

                end;

                  suppose (p1 `1 ) <> (q `1 ) & (p1 `2 ) = (q `2 );

                  hence thesis by A10, A12, Th30;

                end;

              end;

              hence thesis;

            end;

          end;

          hence thesis;

        end;

          suppose

           A22: (q `1 ) <> (p `1 ) & (q `2 ) = (p `2 );

          set r = (p `2 ), pq = { p2 : (p2 `2 ) = r & (p `1 ) <= (p2 `1 ) & (p2 `1 ) <= (q `1 ) }, qp = { p3 : (p3 `2 ) = r & (q `1 ) <= (p3 `1 ) & (p3 `1 ) <= (p `1 ) }, pp1 = { p11 : (p11 `2 ) = r & (p `1 ) <= (p11 `1 ) & (p11 `1 ) <= (p1 `1 ) }, p1p = { p22 : (p22 `2 ) = r & (p1 `1 ) <= (p22 `1 ) & (p22 `1 ) <= (p `1 ) }, qp1 = { q1 : (q1 `2 ) = r & (q `1 ) <= (q1 `1 ) & (q1 `1 ) <= (p1 `1 ) }, p1q = { q2 : (q2 `2 ) = r & (p1 `1 ) <= (q2 `1 ) & (q2 `1 ) <= (q `1 ) };

          now

            per cases by A22, XXREAL_0: 1;

              suppose

               A23: (q `1 ) > (p `1 );

              now

                per cases by A7;

                  suppose (p1 `1 ) = (q `1 ) & (p1 `2 ) <> (q `2 );

                  hence thesis by A10, A22, Th29;

                end;

                  suppose

                   A24: (p1 `1 ) <> (q `1 ) & (p1 `2 ) = (q `2 );

                  now

                    per cases by A24, XXREAL_0: 1;

                      case

                       A25: (p1 `1 ) > (q `1 );

                      then q in pp1 by A22, A23;

                      then q in ( LSeg (p,p1)) by A8, A9, A22, A23, A24, A25, Th10, XXREAL_0: 2;

                      hence thesis by TOPREAL1: 8;

                    end;

                      case

                       A26: (p1 `1 ) < (q `1 );

                      now

                        per cases by XXREAL_0: 1;

                          suppose

                           A27: (p1 `1 ) > (p `1 );

                          then p1 in pq by A22, A24, A26;

                          then p1 in ( LSeg (p,q)) by A8, A10, A22, A26, A27, Th10, XXREAL_0: 2;

                          hence contradiction by A1, A11;

                        end;

                          suppose (p1 `1 ) = (p `1 );

                          hence contradiction by A1, A3, A22, A24, Th6;

                        end;

                          suppose (p1 `1 ) < (p `1 );

                          then p in p1q by A23;

                          hence contradiction by A4, A9, A10, A22, A24, A26, Th10;

                        end;

                      end;

                      hence contradiction;

                    end;

                  end;

                  hence thesis;

                end;

              end;

              hence thesis;

            end;

              suppose

               A28: (q `1 ) < (p `1 );

              now

                per cases by A7;

                  suppose (p1 `1 ) = (q `1 ) & (p1 `2 ) <> (q `2 );

                  hence thesis by A10, A22, Th29;

                end;

                  suppose

                   A29: (p1 `1 ) <> (q `1 ) & (p1 `2 ) = (q `2 );

                  now

                    per cases by A29, XXREAL_0: 1;

                      case

                       A30: (p1 `1 ) > (q `1 );

                      now

                        per cases by XXREAL_0: 1;

                          suppose (p1 `1 ) > (p `1 );

                          then p in qp1 by A28;

                          hence contradiction by A4, A9, A10, A22, A29, A30, Th10;

                        end;

                          suppose (p1 `1 ) = (p `1 );

                          hence contradiction by A1, A3, A22, A29, Th6;

                        end;

                          suppose (p1 `1 ) < (p `1 );

                          then p1 in qp by A22, A29, A30;

                          then p1 in ( LSeg (p,q)) by A8, A10, A22, A28, Th10;

                          hence contradiction by A1, A11;

                        end;

                      end;

                      hence contradiction;

                    end;

                      case

                       A31: (p1 `1 ) < (q `1 );

                      then q in p1p by A22, A28;

                      then q in ( LSeg (p1,p)) by A8, A9, A22, A28, A29, A31, Th10, XXREAL_0: 2;

                      hence thesis by TOPREAL1: 8;

                    end;

                  end;

                  hence thesis;

                end;

              end;

              hence thesis;

            end;

          end;

          hence thesis;

        end;

      end;

      hence thesis;

    end;

    theorem :: TOPREAL3:43

     not p1 in ( Ball (u,r)) & p in ( Ball (u,r)) & |[(p `1 ), (q `2 )]| in ( Ball (u,r)) & not |[(p `1 ), (q `2 )]| in ( LSeg (p1,p)) & (p1 `1 ) = (p `1 ) & (p `1 ) <> (q `1 ) & (p `2 ) <> (q `2 ) implies ((( LSeg (p, |[(p `1 ), (q `2 )]|)) \/ ( LSeg ( |[(p `1 ), (q `2 )]|,q))) /\ ( LSeg (p1,p))) = {p}

    proof

      set v = |[(p `1 ), (q `2 )]|;

      assume that

       A1: not p1 in ( Ball (u,r)) and

       A2: p in ( Ball (u,r)) and

       A3: v in ( Ball (u,r)) and

       A4: not v in ( LSeg (p1,p)) and

       A5: (p1 `1 ) = (p `1 ) and

       A6: (p `1 ) <> (q `1 ) and

       A7: (p `2 ) <> (q `2 );

      

       A8: ( LSeg (p,v)) c= ( Ball (u,r)) by A2, A3, Th21;

      p in ( LSeg (p,v)) by RLTOPSP1: 68;

      then p in ( LSeg (p1,p)) & p in (( LSeg (p,v)) \/ ( LSeg (v,q))) by RLTOPSP1: 68, XBOOLE_0:def 3;

      then p in ((( LSeg (p,v)) \/ ( LSeg (v,q))) /\ ( LSeg (p1,p))) by XBOOLE_0:def 4;

      then

       A9: {p} c= ((( LSeg (p,v)) \/ ( LSeg (v,q))) /\ ( LSeg (p1,p))) by ZFMISC_1: 31;

      

       A10: ((( LSeg (p,v)) \/ ( LSeg (v,q))) /\ ( LSeg (p1,p))) = ((( LSeg (p,v)) /\ ( LSeg (p1,p))) \/ (( LSeg (v,q)) /\ ( LSeg (p1,p)))) by XBOOLE_1: 23;

      

       A11: p1 = |[(p `1 ), (p1 `2 )]| by A5, EUCLID: 53;

      

       A12: q = |[(q `1 ), (q `2 )]| by EUCLID: 53;

      

       A13: p = |[(p `1 ), (p `2 )]| by EUCLID: 53;

      

       A14: (v `1 ) = (p `1 ) by EUCLID: 52;

      

       A15: (v `2 ) = (q `2 ) by EUCLID: 52;

      per cases ;

        suppose (p1 `2 ) = (p `2 );

        hence thesis by A1, A2, A5, Th6;

      end;

        suppose

         A16: (p1 `2 ) <> (p `2 );

        now

          per cases by A16, XXREAL_0: 1;

            suppose

             A17: (p1 `2 ) > (p `2 );

            now

              per cases by A6, XXREAL_0: 1;

                suppose

                 A18: (p `1 ) > (q `1 );

                now

                  per cases by A7, XXREAL_0: 1;

                    case

                     A19: (p `2 ) > (q `2 );

                    then

                     A20: (p `2 ) >= (v `2 ) by EUCLID: 52;

                    ((( LSeg (p,v)) \/ ( LSeg (v,q))) /\ ( LSeg (p1,p))) c= {p}

                    proof

                      let x be object such that

                       A21: x in ((( LSeg (p,v)) \/ ( LSeg (v,q))) /\ ( LSeg (p1,p)));

                      now

                        per cases by A10, A21, XBOOLE_0:def 3;

                          case

                           A22: x in (( LSeg (p,v)) /\ ( LSeg (p1,p)));

                          p in { q1 : (q1 `1 ) = (p `1 ) & (v `2 ) <= (q1 `2 ) & (q1 `2 ) <= (p1 `2 ) } by A17, A20;

                          then p in ( LSeg (p1,v)) by A11, A15, A17, A19, Th9, XXREAL_0: 2;

                          hence thesis by A22, TOPREAL1: 8;

                        end;

                          case

                           A23: x in (( LSeg (v,q)) /\ ( LSeg (p1,p)));

                          then x in ( LSeg (v,q)) by XBOOLE_0:def 4;

                          then x in { p2 : (p2 `2 ) = (q `2 ) & (q `1 ) <= (p2 `1 ) & (p2 `1 ) <= (p `1 ) } by A12, A18, Th10;

                          then

                           A24: ex p2 st p2 = x & (p2 `2 ) = (q `2 ) & (q `1 ) <= (p2 `1 ) & (p2 `1 ) <= (p `1 );

                          x in ( LSeg (p1,p)) by A23, XBOOLE_0:def 4;

                          then x in { q2 : (q2 `1 ) = (p `1 ) & (p `2 ) <= (q2 `2 ) & (q2 `2 ) <= (p1 `2 ) } by A11, A13, A17, Th9;

                          then ex q2 st q2 = x & (q2 `1 ) = (p `1 ) & (p `2 ) <= (q2 `2 ) & (q2 `2 ) <= (p1 `2 );

                          hence contradiction by A19, A24;

                        end;

                      end;

                      hence thesis;

                    end;

                    hence thesis by A9;

                  end;

                    case

                     A25: (p `2 ) < (q `2 );

                    now

                      per cases by XXREAL_0: 1;

                        suppose

                         A26: (q `2 ) > (p1 `2 );

                        then p1 in { q2 : (q2 `1 ) = (p `1 ) & (p `2 ) <= (q2 `2 ) & (q2 `2 ) <= (v `2 ) } by A5, A15, A17;

                        then p1 in ( LSeg (p,v)) by A13, A15, A17, A26, Th9, XXREAL_0: 2;

                        hence contradiction by A1, A8;

                      end;

                        suppose (q `2 ) = (p1 `2 );

                        hence contradiction by A1, A3, A5, EUCLID: 53;

                      end;

                        suppose

                         A27: (q `2 ) < (p1 `2 );

                        then v in { p2 : (p2 `1 ) = (p `1 ) & (p `2 ) <= (p2 `2 ) & (p2 `2 ) <= (p1 `2 ) } by A14, A15, A25;

                        hence contradiction by A4, A11, A13, A25, A27, Th9, XXREAL_0: 2;

                      end;

                    end;

                    hence contradiction;

                  end;

                end;

                hence thesis;

              end;

                suppose

                 A28: (p `1 ) < (q `1 );

                now

                  per cases by A7, XXREAL_0: 1;

                    case

                     A29: (p `2 ) > (q `2 );

                    then

                     A30: (p `2 ) >= (v `2 ) by EUCLID: 52;

                    ((( LSeg (p,v)) \/ ( LSeg (v,q))) /\ ( LSeg (p1,p))) c= {p}

                    proof

                      let x be object such that

                       A31: x in ((( LSeg (p,v)) \/ ( LSeg (v,q))) /\ ( LSeg (p1,p)));

                      now

                        per cases by A10, A31, XBOOLE_0:def 3;

                          case

                           A32: x in (( LSeg (p,v)) /\ ( LSeg (p1,p)));

                          p in { q1 : (q1 `1 ) = (p `1 ) & (v `2 ) <= (q1 `2 ) & (q1 `2 ) <= (p1 `2 ) } by A17, A30;

                          then p in ( LSeg (p1,v)) by A11, A15, A17, A29, Th9, XXREAL_0: 2;

                          hence thesis by A32, TOPREAL1: 8;

                        end;

                          case

                           A33: x in (( LSeg (v,q)) /\ ( LSeg (p1,p)));

                          then x in ( LSeg (v,q)) by XBOOLE_0:def 4;

                          then x in { p2 : (p2 `2 ) = (q `2 ) & (p `1 ) <= (p2 `1 ) & (p2 `1 ) <= (q `1 ) } by A12, A28, Th10;

                          then

                           A34: ex p2 st p2 = x & (p2 `2 ) = (q `2 ) & (p `1 ) <= (p2 `1 ) & (p2 `1 ) <= (q `1 );

                          x in ( LSeg (p1,p)) by A33, XBOOLE_0:def 4;

                          then x in { q2 : (q2 `1 ) = (p `1 ) & (p `2 ) <= (q2 `2 ) & (q2 `2 ) <= (p1 `2 ) } by A11, A13, A17, Th9;

                          then ex q2 st q2 = x & (q2 `1 ) = (p `1 ) & (p `2 ) <= (q2 `2 ) & (q2 `2 ) <= (p1 `2 );

                          hence contradiction by A29, A34;

                        end;

                      end;

                      hence thesis;

                    end;

                    hence thesis by A9;

                  end;

                    case

                     A35: (p `2 ) < (q `2 );

                    now

                      per cases by XXREAL_0: 1;

                        suppose

                         A36: (q `2 ) > (p1 `2 );

                        then p1 in { q2 : (q2 `1 ) = (p `1 ) & (p `2 ) <= (q2 `2 ) & (q2 `2 ) <= (v `2 ) } by A5, A15, A17;

                        then p1 in ( LSeg (p,v)) by A13, A15, A17, A36, Th9, XXREAL_0: 2;

                        hence contradiction by A1, A8;

                      end;

                        suppose (q `2 ) = (p1 `2 );

                        hence contradiction by A1, A3, A5, EUCLID: 53;

                      end;

                        suppose

                         A37: (q `2 ) < (p1 `2 );

                        then v in { p2 : (p2 `1 ) = (p `1 ) & (p `2 ) <= (p2 `2 ) & (p2 `2 ) <= (p1 `2 ) } by A14, A15, A35;

                        hence contradiction by A4, A11, A13, A35, A37, Th9, XXREAL_0: 2;

                      end;

                    end;

                    hence contradiction;

                  end;

                end;

                hence thesis;

              end;

            end;

            hence thesis;

          end;

            suppose

             A38: (p1 `2 ) < (p `2 );

            now

              per cases by A6, XXREAL_0: 1;

                suppose

                 A39: (p `1 ) > (q `1 );

                now

                  per cases by A7, XXREAL_0: 1;

                    case

                     A40: (p `2 ) > (q `2 );

                    now

                      per cases by XXREAL_0: 1;

                        suppose

                         A41: (q `2 ) > (p1 `2 );

                        then v in { p2 : (p2 `1 ) = (p `1 ) & (p1 `2 ) <= (p2 `2 ) & (p2 `2 ) <= (p `2 ) } by A14, A15, A40;

                        hence contradiction by A4, A11, A13, A40, A41, Th9, XXREAL_0: 2;

                      end;

                        suppose (q `2 ) = (p1 `2 );

                        hence contradiction by A1, A3, A5, EUCLID: 53;

                      end;

                        suppose

                         A42: (q `2 ) < (p1 `2 );

                        then p1 in { q2 : (q2 `1 ) = (p `1 ) & (v `2 ) <= (q2 `2 ) & (q2 `2 ) <= (p `2 ) } by A5, A15, A38;

                        then p1 in ( LSeg (p,v)) by A13, A15, A38, A42, Th9, XXREAL_0: 2;

                        hence contradiction by A1, A8;

                      end;

                    end;

                    hence contradiction;

                  end;

                    case

                     A43: (p `2 ) < (q `2 );

                    ((( LSeg (p,v)) \/ ( LSeg (v,q))) /\ ( LSeg (p1,p))) c= {p}

                    proof

                      let x be object such that

                       A44: x in ((( LSeg (p,v)) \/ ( LSeg (v,q))) /\ ( LSeg (p1,p)));

                      now

                        per cases by A10, A44, XBOOLE_0:def 3;

                          case

                           A45: x in (( LSeg (p,v)) /\ ( LSeg (p1,p)));

                          p in { q1 : (q1 `1 ) = (p `1 ) & (p1 `2 ) <= (q1 `2 ) & (q1 `2 ) <= (v `2 ) } by A15, A38, A43;

                          then p in ( LSeg (p1,v)) by A11, A15, A38, A43, Th9, XXREAL_0: 2;

                          hence thesis by A45, TOPREAL1: 8;

                        end;

                          case

                           A46: x in (( LSeg (v,q)) /\ ( LSeg (p1,p)));

                          then x in ( LSeg (v,q)) by XBOOLE_0:def 4;

                          then x in { p2 : (p2 `2 ) = (q `2 ) & (q `1 ) <= (p2 `1 ) & (p2 `1 ) <= (p `1 ) } by A12, A39, Th10;

                          then

                           A47: ex p2 st p2 = x & (p2 `2 ) = (q `2 ) & (q `1 ) <= (p2 `1 ) & (p2 `1 ) <= (p `1 );

                          x in ( LSeg (p1,p)) by A46, XBOOLE_0:def 4;

                          then x in { q2 : (q2 `1 ) = (p `1 ) & (p1 `2 ) <= (q2 `2 ) & (q2 `2 ) <= (p `2 ) } by A11, A13, A38, Th9;

                          then ex q2 st q2 = x & (q2 `1 ) = (p `1 ) & (p1 `2 ) <= (q2 `2 ) & (q2 `2 ) <= (p `2 );

                          hence contradiction by A43, A47;

                        end;

                      end;

                      hence thesis;

                    end;

                    hence thesis by A9;

                  end;

                end;

                hence thesis;

              end;

                suppose

                 A48: (p `1 ) < (q `1 );

                now

                  per cases by A7, XXREAL_0: 1;

                    case

                     A49: (p `2 ) > (q `2 );

                    now

                      per cases by XXREAL_0: 1;

                        suppose

                         A50: (q `2 ) > (p1 `2 );

                        then v in { p2 : (p2 `1 ) = (p `1 ) & (p1 `2 ) <= (p2 `2 ) & (p2 `2 ) <= (p `2 ) } by A14, A15, A49;

                        hence contradiction by A4, A11, A13, A49, A50, Th9, XXREAL_0: 2;

                      end;

                        suppose (q `2 ) = (p1 `2 );

                        hence contradiction by A1, A3, A5, EUCLID: 53;

                      end;

                        suppose

                         A51: (q `2 ) < (p1 `2 );

                        then p1 in { q2 : (q2 `1 ) = (p `1 ) & (v `2 ) <= (q2 `2 ) & (q2 `2 ) <= (p `2 ) } by A5, A15, A38;

                        then p1 in ( LSeg (p,v)) by A13, A15, A38, A51, Th9, XXREAL_0: 2;

                        hence contradiction by A1, A8;

                      end;

                    end;

                    hence contradiction;

                  end;

                    case

                     A52: (p `2 ) < (q `2 );

                    ((( LSeg (p,v)) \/ ( LSeg (v,q))) /\ ( LSeg (p1,p))) c= {p}

                    proof

                      let x be object such that

                       A53: x in ((( LSeg (p,v)) \/ ( LSeg (v,q))) /\ ( LSeg (p1,p)));

                      now

                        per cases by A10, A53, XBOOLE_0:def 3;

                          case

                           A54: x in (( LSeg (p,v)) /\ ( LSeg (p1,p)));

                          p in { q1 : (q1 `1 ) = (p `1 ) & (p1 `2 ) <= (q1 `2 ) & (q1 `2 ) <= (v `2 ) } by A15, A38, A52;

                          then p in ( LSeg (p1,v)) by A11, A15, A38, A52, Th9, XXREAL_0: 2;

                          hence thesis by A54, TOPREAL1: 8;

                        end;

                          case

                           A55: x in (( LSeg (v,q)) /\ ( LSeg (p1,p)));

                          then x in ( LSeg (v,q)) by XBOOLE_0:def 4;

                          then x in { p2 : (p2 `2 ) = (q `2 ) & (p `1 ) <= (p2 `1 ) & (p2 `1 ) <= (q `1 ) } by A12, A48, Th10;

                          then

                           A56: ex p2 st p2 = x & (p2 `2 ) = (q `2 ) & (p `1 ) <= (p2 `1 ) & (p2 `1 ) <= (q `1 );

                          x in ( LSeg (p1,p)) by A55, XBOOLE_0:def 4;

                          then x in { q2 : (q2 `1 ) = (p `1 ) & (p1 `2 ) <= (q2 `2 ) & (q2 `2 ) <= (p `2 ) } by A11, A13, A38, Th9;

                          then ex q2 st q2 = x & (q2 `1 ) = (p `1 ) & (p1 `2 ) <= (q2 `2 ) & (q2 `2 ) <= (p `2 );

                          hence contradiction by A52, A56;

                        end;

                      end;

                      hence thesis;

                    end;

                    hence thesis by A9;

                  end;

                end;

                hence thesis;

              end;

            end;

            hence thesis;

          end;

        end;

        hence thesis;

      end;

    end;

    theorem :: TOPREAL3:44

     not p1 in ( Ball (u,r)) & p in ( Ball (u,r)) & |[(q `1 ), (p `2 )]| in ( Ball (u,r)) & not |[(q `1 ), (p `2 )]| in ( LSeg (p1,p)) & (p1 `2 ) = (p `2 ) & (p `1 ) <> (q `1 ) & (p `2 ) <> (q `2 ) implies ((( LSeg (p, |[(q `1 ), (p `2 )]|)) \/ ( LSeg ( |[(q `1 ), (p `2 )]|,q))) /\ ( LSeg (p1,p))) = {p}

    proof

      set v = |[(q `1 ), (p `2 )]|;

      assume that

       A1: not p1 in ( Ball (u,r)) and

       A2: p in ( Ball (u,r)) and

       A3: v in ( Ball (u,r)) and

       A4: not v in ( LSeg (p1,p)) and

       A5: (p1 `2 ) = (p `2 ) and

       A6: (p `1 ) <> (q `1 ) and

       A7: (p `2 ) <> (q `2 );

      

       A8: ( LSeg (p,v)) c= ( Ball (u,r)) by A2, A3, Th21;

      

       A9: p1 = |[(p1 `1 ), (p `2 )]| by A5, EUCLID: 53;

      p in ( LSeg (p,v)) by RLTOPSP1: 68;

      then p in ( LSeg (p1,p)) & p in (( LSeg (p,v)) \/ ( LSeg (v,q))) by RLTOPSP1: 68, XBOOLE_0:def 3;

      then p in ((( LSeg (p,v)) \/ ( LSeg (v,q))) /\ ( LSeg (p1,p))) by XBOOLE_0:def 4;

      then

       A10: {p} c= ((( LSeg (p,v)) \/ ( LSeg (v,q))) /\ ( LSeg (p1,p))) by ZFMISC_1: 31;

      

       A11: ((( LSeg (p,v)) \/ ( LSeg (v,q))) /\ ( LSeg (p1,p))) = ((( LSeg (p,v)) /\ ( LSeg (p1,p))) \/ (( LSeg (v,q)) /\ ( LSeg (p1,p)))) by XBOOLE_1: 23;

      

       A12: q = |[(q `1 ), (q `2 )]| by EUCLID: 53;

      

       A13: p = |[(p `1 ), (p `2 )]| by EUCLID: 53;

      

       A14: (v `2 ) = (p `2 ) by EUCLID: 52;

      

       A15: (v `1 ) = (q `1 ) by EUCLID: 52;

      per cases ;

        suppose (p1 `1 ) = (p `1 );

        hence thesis by A1, A2, A5, Th6;

      end;

        suppose

         A16: (p1 `1 ) <> (p `1 );

        now

          per cases by A16, XXREAL_0: 1;

            suppose

             A17: (p1 `1 ) > (p `1 );

            now

              per cases by A6, XXREAL_0: 1;

                case

                 A18: (p `1 ) > (q `1 );

                then

                 A19: (p `1 ) >= (v `1 ) by EUCLID: 52;

                now

                  per cases by A7, XXREAL_0: 1;

                    suppose

                     A20: (p `2 ) > (q `2 );

                    ((( LSeg (p,v)) \/ ( LSeg (v,q))) /\ ( LSeg (p1,p))) c= {p}

                    proof

                      let x be object such that

                       A21: x in ((( LSeg (p,v)) \/ ( LSeg (v,q))) /\ ( LSeg (p1,p)));

                      now

                        per cases by A11, A21, XBOOLE_0:def 3;

                          case

                           A22: x in (( LSeg (p,v)) /\ ( LSeg (p1,p)));

                          p in { q1 : (q1 `2 ) = (p `2 ) & (v `1 ) <= (q1 `1 ) & (q1 `1 ) <= (p1 `1 ) } by A17, A19;

                          then p in ( LSeg (p1,v)) by A9, A15, A17, A18, Th10, XXREAL_0: 2;

                          hence thesis by A22, TOPREAL1: 8;

                        end;

                          case

                           A23: x in (( LSeg (v,q)) /\ ( LSeg (p1,p)));

                          then x in ( LSeg (q,v)) by XBOOLE_0:def 4;

                          then x in { p2 : (p2 `1 ) = (q `1 ) & (q `2 ) <= (p2 `2 ) & (p2 `2 ) <= (p `2 ) } by A12, A20, Th9;

                          then

                           A24: ex p2 st p2 = x & (p2 `1 ) = (q `1 ) & (q `2 ) <= (p2 `2 ) & (p2 `2 ) <= (p `2 );

                          x in ( LSeg (p,p1)) by A23, XBOOLE_0:def 4;

                          then x in { q2 : (q2 `2 ) = (p `2 ) & (p `1 ) <= (q2 `1 ) & (q2 `1 ) <= (p1 `1 ) } by A9, A13, A17, Th10;

                          then ex q2 st q2 = x & (q2 `2 ) = (p `2 ) & (p `1 ) <= (q2 `1 ) & (q2 `1 ) <= (p1 `1 );

                          hence contradiction by A18, A24;

                        end;

                      end;

                      hence thesis;

                    end;

                    hence thesis by A10;

                  end;

                    suppose

                     A25: (p `2 ) < (q `2 );

                    ((( LSeg (p,v)) \/ ( LSeg (v,q))) /\ ( LSeg (p1,p))) c= {p}

                    proof

                      let x be object such that

                       A26: x in ((( LSeg (p,v)) \/ ( LSeg (v,q))) /\ ( LSeg (p1,p)));

                      now

                        per cases by A11, A26, XBOOLE_0:def 3;

                          case

                           A27: x in (( LSeg (p,v)) /\ ( LSeg (p1,p)));

                          p in { q1 : (q1 `2 ) = (p `2 ) & (v `1 ) <= (q1 `1 ) & (q1 `1 ) <= (p1 `1 ) } by A17, A19;

                          then p in ( LSeg (p1,v)) by A9, A15, A17, A18, Th10, XXREAL_0: 2;

                          hence thesis by A27, TOPREAL1: 8;

                        end;

                          case

                           A28: x in (( LSeg (v,q)) /\ ( LSeg (p1,p)));

                          then x in ( LSeg (p1,p)) by XBOOLE_0:def 4;

                          then x in { q2 : (q2 `2 ) = (p `2 ) & (p `1 ) <= (q2 `1 ) & (q2 `1 ) <= (p1 `1 ) } by A9, A13, A17, Th10;

                          then

                           A29: ex q2 st q2 = x & (q2 `2 ) = (p `2 ) & (p `1 ) <= (q2 `1 ) & (q2 `1 ) <= (p1 `1 );

                          x in ( LSeg (v,q)) by A28, XBOOLE_0:def 4;

                          then x in { p2 : (p2 `1 ) = (q `1 ) & (v `2 ) <= (p2 `2 ) & (p2 `2 ) <= (q `2 ) } by A12, A14, A25, Th9;

                          then ex p2 st p2 = x & (p2 `1 ) = (q `1 ) & (v `2 ) <= (p2 `2 ) & (p2 `2 ) <= (q `2 );

                          hence contradiction by A18, A29;

                        end;

                      end;

                      hence thesis;

                    end;

                    hence thesis by A10;

                  end;

                end;

                hence thesis;

              end;

                case

                 A30: (p `1 ) < (q `1 );

                now

                  per cases by XXREAL_0: 1;

                    suppose

                     A31: (q `1 ) > (p1 `1 );

                    then p1 in { q2 : (q2 `2 ) = (p `2 ) & (p `1 ) <= (q2 `1 ) & (q2 `1 ) <= (v `1 ) } by A5, A15, A17;

                    then p1 in ( LSeg (p,v)) by A13, A15, A17, A31, Th10, XXREAL_0: 2;

                    hence contradiction by A1, A8;

                  end;

                    suppose (q `1 ) = (p1 `1 );

                    hence contradiction by A1, A3, A5, EUCLID: 53;

                  end;

                    suppose (q `1 ) < (p1 `1 );

                    then v in { p2 : (p2 `2 ) = (p `2 ) & (p `1 ) <= (p2 `1 ) & (p2 `1 ) <= (p1 `1 ) } by A15, A14, A30;

                    hence contradiction by A4, A9, A13, A17, Th10;

                  end;

                end;

                hence contradiction;

              end;

            end;

            hence thesis;

          end;

            suppose

             A32: (p1 `1 ) < (p `1 );

            now

              per cases by A6, XXREAL_0: 1;

                case

                 A33: (p `1 ) > (q `1 );

                now

                  per cases by XXREAL_0: 1;

                    suppose (q `1 ) > (p1 `1 );

                    then v in { q2 : (q2 `2 ) = (p `2 ) & (p1 `1 ) <= (q2 `1 ) & (q2 `1 ) <= (p `1 ) } by A15, A14, A33;

                    hence contradiction by A4, A9, A13, A32, Th10;

                  end;

                    suppose (q `1 ) = (p1 `1 );

                    hence contradiction by A1, A3, A5, EUCLID: 53;

                  end;

                    suppose

                     A34: (q `1 ) < (p1 `1 );

                    then p1 in { p2 : (p2 `2 ) = (p `2 ) & (v `1 ) <= (p2 `1 ) & (p2 `1 ) <= (p `1 ) } by A5, A15, A32;

                    then p1 in ( LSeg (p,v)) by A13, A15, A32, A34, Th10, XXREAL_0: 2;

                    hence contradiction by A1, A8;

                  end;

                end;

                hence contradiction;

              end;

                case

                 A35: (p `1 ) < (q `1 );

                then

                 A36: (p `1 ) <= (v `1 ) by EUCLID: 52;

                now

                  per cases by A7, XXREAL_0: 1;

                    suppose

                     A37: (p `2 ) > (q `2 );

                    ((( LSeg (p,v)) \/ ( LSeg (v,q))) /\ ( LSeg (p1,p))) c= {p}

                    proof

                      let x be object such that

                       A38: x in ((( LSeg (p,v)) \/ ( LSeg (v,q))) /\ ( LSeg (p1,p)));

                      now

                        per cases by A11, A38, XBOOLE_0:def 3;

                          case

                           A39: x in (( LSeg (p,v)) /\ ( LSeg (p1,p)));

                          p in { q1 : (q1 `2 ) = (p `2 ) & (p1 `1 ) <= (q1 `1 ) & (q1 `1 ) <= (v `1 ) } by A32, A36;

                          then p in ( LSeg (p1,v)) by A9, A15, A32, A35, Th10, XXREAL_0: 2;

                          hence thesis by A39, TOPREAL1: 8;

                        end;

                          case

                           A40: x in (( LSeg (v,q)) /\ ( LSeg (p1,p)));

                          then x in ( LSeg (v,q)) by XBOOLE_0:def 4;

                          then x in { p2 : (p2 `1 ) = (q `1 ) & (q `2 ) <= (p2 `2 ) & (p2 `2 ) <= (p `2 ) } by A12, A37, Th9;

                          then

                           A41: ex p2 st p2 = x & (p2 `1 ) = (q `1 ) & (q `2 ) <= (p2 `2 ) & (p2 `2 ) <= (p `2 );

                          x in ( LSeg (p1,p)) by A40, XBOOLE_0:def 4;

                          then x in { q2 : (q2 `2 ) = (p `2 ) & (p1 `1 ) <= (q2 `1 ) & (q2 `1 ) <= (p `1 ) } by A9, A13, A32, Th10;

                          then ex q2 st q2 = x & (q2 `2 ) = (p `2 ) & (p1 `1 ) <= (q2 `1 ) & (q2 `1 ) <= (p `1 );

                          hence contradiction by A35, A41;

                        end;

                      end;

                      hence thesis;

                    end;

                    hence thesis by A10;

                  end;

                    suppose

                     A42: (p `2 ) < (q `2 );

                    ((( LSeg (p,v)) \/ ( LSeg (v,q))) /\ ( LSeg (p1,p))) c= {p}

                    proof

                      let x be object such that

                       A43: x in ((( LSeg (p,v)) \/ ( LSeg (v,q))) /\ ( LSeg (p1,p)));

                      now

                        per cases by A11, A43, XBOOLE_0:def 3;

                          case

                           A44: x in (( LSeg (p,v)) /\ ( LSeg (p1,p)));

                          p in { q1 : (q1 `2 ) = (p `2 ) & (p1 `1 ) <= (q1 `1 ) & (q1 `1 ) <= (v `1 ) } by A32, A36;

                          then p in ( LSeg (p1,v)) by A9, A15, A32, A35, Th10, XXREAL_0: 2;

                          hence thesis by A44, TOPREAL1: 8;

                        end;

                          case

                           A45: x in (( LSeg (v,q)) /\ ( LSeg (p1,p)));

                          then x in ( LSeg (p1,p)) by XBOOLE_0:def 4;

                          then x in { q2 : (q2 `2 ) = (p `2 ) & (p1 `1 ) <= (q2 `1 ) & (q2 `1 ) <= (p `1 ) } by A9, A13, A32, Th10;

                          then

                           A46: ex q2 st q2 = x & (q2 `2 ) = (p `2 ) & (p1 `1 ) <= (q2 `1 ) & (q2 `1 ) <= (p `1 );

                          x in ( LSeg (v,q)) by A45, XBOOLE_0:def 4;

                          then x in { p2 : (p2 `1 ) = (q `1 ) & (v `2 ) <= (p2 `2 ) & (p2 `2 ) <= (q `2 ) } by A12, A14, A42, Th9;

                          then ex p2 st p2 = x & (p2 `1 ) = (q `1 ) & (v `2 ) <= (p2 `2 ) & (p2 `2 ) <= (q `2 );

                          hence contradiction by A35, A46;

                        end;

                      end;

                      hence thesis;

                    end;

                    hence thesis by A10;

                  end;

                end;

                hence thesis;

              end;

            end;

            hence thesis;

          end;

        end;

        hence thesis;

      end;

    end;

    reserve f for FinSequence of REAL ;

    theorem :: TOPREAL3:45

    

     Th45: ( len f) = n implies f in the carrier of ( Euclid n)

    proof

      f in ( REAL * ) & (n -tuples_on REAL ) = { s where s be Element of ( REAL * ) : ( len s) = n } by FINSEQ_1:def 11, FINSEQ_2:def 4;

      hence thesis;

    end;

    theorem :: TOPREAL3:46

    ( len f) = n implies f in the carrier of ( TOP-REAL n)

    proof

      assume ( len f) = n;

      then f in the carrier of ( Euclid n) by Th45;

      hence thesis by Th8;

    end;