tbsp_1.miz



    begin

    reserve M for non empty MetrSpace,

c,g1,g2 for Element of M;

    reserve N for non empty MetrStruct,

w for Element of N,

G for Subset-Family of N,

C for Subset of N;

    reserve R for Reflexive non empty MetrStruct;

    reserve T for Reflexive symmetric triangle non empty MetrStruct,

t1 for Element of T,

Y for Subset-Family of T,

P for Subset of T;

    reserve f for Function,

n,m,p,n1,n2,k for Nat,

r,s,L for Real,

x,y for set;

    theorem :: TBSP_1:1

    

     Th1: for L st 0 < L & L < 1 holds for n, m st n <= m holds (L to_power m) <= (L to_power n)

    proof

      let L such that

       A1: 0 < L & L < 1;

      let n, m such that

       A2: n <= m;

      per cases by A2, XXREAL_0: 1;

        suppose n < m;

        hence thesis by A1, POWER: 40;

      end;

        suppose n = m;

        hence thesis;

      end;

    end;

    theorem :: TBSP_1:2

    

     Th2: for L st 0 < L & L < 1 holds for k holds (L to_power k) <= 1 & 0 < (L to_power k)

    proof

      let L;

      assume that

       A1: 0 < L and

       A2: L < 1;

      defpred X[ Nat] means (L to_power $1) <= 1 & 0 < (L to_power $1);

      

       A3: for k st X[k] holds X[(k + 1)]

      proof

        let k be Nat such that

         A4: (L to_power k) <= 1 and

         A5: 0 < (L to_power k);

        

         A6: (L to_power (k + 1)) = ((L to_power k) * (L to_power 1)) by A1, POWER: 27

        .= ((L to_power k) * L) by POWER: 25;

        ((L to_power k) * L) <= (L to_power k) by A2, A5, XREAL_1: 153;

        hence thesis by A1, A4, A5, A6, XREAL_1: 129, XXREAL_0: 2;

      end;

      

       A7: X[ 0 ] by POWER: 24;

      thus for k holds X[k] from NAT_1:sch 2( A7, A3);

    end;

    theorem :: TBSP_1:3

    

     Th3: for L st 0 < L & L < 1 holds for s st 0 < s holds ex n st (L to_power n) < s

    proof

      let L such that

       A1: 0 < L & L < 1;

      let s;

      deffunc U( Nat) = (L to_power ($1 + 1));

      consider rseq be Real_Sequence such that

       A2: for n be Nat holds (rseq . n) = U(n) from SEQ_1:sch 1;

      assume

       A3: 0 < s;

      rseq is convergent & ( lim rseq) = 0 by A1, A2, SERIES_1: 1;

      then

      consider n be Nat such that

       A4: for m be Nat st n <= m holds |.((rseq . m) - 0 ).| < s by A3, SEQ_2:def 7;

      take (n + 1);

      

       A5: 0 < (L to_power (n + 1)) by A1, Th2;

       |.((rseq . n) - 0 ).| = |.(L to_power (n + 1)).| by A2

      .= (L to_power (n + 1)) by A5, ABSVALUE:def 1;

      hence thesis by A4;

    end;

    definition

      let N;

      :: TBSP_1:def1

      attr N is totally_bounded means for r st r > 0 holds ex G st G is finite & the carrier of N = ( union G) & for C st C in G holds ex w st C = ( Ball (w,r));

    end

    reserve S1 for sequence of M,

S2 for sequence of N;

    

     Lm1: f is sequence of N iff (( dom f) = NAT & for x st x in NAT holds (f . x) is Element of N)

    proof

      thus f is sequence of N implies (( dom f) = NAT & for x st x in NAT holds (f . x) is Element of N)

      proof

        assume

         A1: f is sequence of N;

        hence ( dom f) = NAT by FUNCT_2:def 1;

        let x;

        assume x in NAT ;

        then x in ( dom f) by A1, FUNCT_2:def 1;

        then

         A2: (f . x) in ( rng f) by FUNCT_1:def 3;

        ( rng f) c= the carrier of N by A1, RELAT_1:def 19;

        hence thesis by A2;

      end;

      assume that

       A3: ( dom f) = NAT and

       A4: for x st x in NAT holds (f . x) is Element of N;

      now

        let y be object;

        assume y in ( rng f);

        then

        consider x be object such that

         A5: x in ( dom f) and

         A6: y = (f . x) by FUNCT_1:def 3;

        (f . x) is Element of N by A3, A4, A5;

        hence y in the carrier of N by A6;

      end;

      then ( rng f) c= the carrier of N;

      hence thesis by A3, FUNCT_2:def 1, RELSET_1: 4;

    end;

    theorem :: TBSP_1:4

    f is sequence of N iff ( dom f) = NAT & for n holds (f . n) is Element of N

    proof

      thus f is sequence of N implies ( dom f) = NAT & for n holds (f . n) is Element of N by Lm1, ORDINAL1:def 12;

      assume that

       A1: ( dom f) = NAT and

       A2: for n holds (f . n) is Element of N;

      for x holds x in NAT implies (f . x) is Element of N by A2;

      hence thesis by A1, Lm1;

    end;

    definition

      let N, S2;

      :: TBSP_1:def2

      attr S2 is convergent means ex x be Element of N st for r st r > 0 holds ex n st for m st n <= m holds ( dist ((S2 . m),x)) < r;

    end

    definition

      let M, S1;

      assume

       A1: S1 is convergent;

      :: TBSP_1:def3

      func lim S1 -> Element of M means for r st r > 0 holds ex n st for m st m >= n holds ( dist ((S1 . m),it )) < r;

      existence by A1;

      uniqueness

      proof

        given g1, g2 such that

         A2: for r st r > 0 holds ex n st for m st n <= m holds ( dist ((S1 . m),g1)) < r and

         A3: for r st r > 0 holds ex n st for m st n <= m holds ( dist ((S1 . m),g2)) < r and

         A4: g1 <> g2;

        set a = (( dist (g1,g2)) / 4);

        

         A5: ( dist (g1,g2)) >= 0 by METRIC_1: 5;

        

         A6: ( dist (g1,g2)) <> 0 by A4, METRIC_1: 2;

        then

        consider n1 such that

         A7: for m st n1 <= m holds ( dist ((S1 . m),g1)) < a by A2, A5, XREAL_1: 224;

        consider n2 such that

         A8: for m st n2 <= m holds ( dist ((S1 . m),g2)) < a by A3, A6, A5, XREAL_1: 224;

        set k = (n1 + n2);

        

         A9: ( dist ((S1 . k),g2)) < a by A8, NAT_1: 12;

        

         A10: ( dist (g1,g2)) <= (( dist (g1,(S1 . k))) + ( dist ((S1 . k),g2))) by METRIC_1: 4;

        ( dist ((S1 . k),g1)) < a by A7, NAT_1: 12;

        then (( dist (g1,(S1 . k))) + ( dist ((S1 . k),g2))) < (a + a) by A9, XREAL_1: 8;

        then ( dist (g1,g2)) < (( dist (g1,g2)) / 2) by A10, XXREAL_0: 2;

        hence contradiction by A6, A5, XREAL_1: 216;

      end;

    end

    definition

      let N, S2;

      :: TBSP_1:def4

      attr S2 is Cauchy means for r st r > 0 holds ex p st for n, m st p <= n & p <= m holds ( dist ((S2 . n),(S2 . m))) < r;

    end

    definition

      let N;

      :: TBSP_1:def5

      attr N is complete means for S2 st S2 is Cauchy holds S2 is convergent;

    end

    theorem :: TBSP_1:5

    

     Th5: N is triangle symmetric & S2 is convergent implies S2 is Cauchy

    proof

      assume that

       A1: N is triangle and

       A2: N is symmetric;

      reconsider N as symmetric non empty MetrStruct by A2;

      assume

       A3: S2 is convergent;

      reconsider S2 as sequence of N;

      consider g be Element of N such that

       A4: for r st 0 < r holds ex n st for m st n <= m holds ( dist ((S2 . m),g)) < r by A3;

      let r;

      assume 0 < r;

      then

      consider n such that

       A5: for m st n <= m holds ( dist ((S2 . m),g)) < (r / 2) by A4, XREAL_1: 215;

      take n;

      let m,m9 be Nat;

      assume that

       A6: m >= n and

       A7: m9 >= n;

      

       A8: ( dist ((S2 . m9),g)) < (r / 2) by A5, A7;

      ( dist ((S2 . m),g)) < (r / 2) by A5, A6;

      then

       A9: (( dist ((S2 . m),g)) + ( dist (g,(S2 . m9)))) < ((r / 2) + (r / 2)) by A8, XREAL_1: 8;

      ( dist ((S2 . m),(S2 . m9))) <= (( dist ((S2 . m),g)) + ( dist (g,(S2 . m9)))) by A1, METRIC_1: 4;

      hence thesis by A9, XXREAL_0: 2;

    end;

    registration

      let M be triangle symmetric non empty MetrStruct;

      cluster convergent -> Cauchy for sequence of M;

      coherence by Th5;

    end

    theorem :: TBSP_1:6

    

     Th6: for N be symmetric non empty MetrStruct, S2 be sequence of N holds S2 is Cauchy iff for r st r > 0 holds ex p st for n, k st p <= n holds ( dist ((S2 . (n + k)),(S2 . n))) < r

    proof

      let N be symmetric non empty MetrStruct, S2 be sequence of N;

      thus S2 is Cauchy implies for r st r > 0 holds ex p st for n, k st p <= n holds ( dist ((S2 . (n + k)),(S2 . n))) < r

      proof

        assume

         A1: S2 is Cauchy;

        let r;

        assume 0 < r;

        then

        consider p such that

         A2: for n, m st p <= n & p <= m holds ( dist ((S2 . n),(S2 . m))) < r by A1;

        take p;

        let n,k be Nat such that

         A3: p <= n;

        n <= (n + k) by NAT_1: 11;

        then p <= (n + k) by A3, XXREAL_0: 2;

        hence thesis by A2, A3;

      end;

      assume

       A4: for r st r > 0 holds ex p st for n, k st p <= n holds ( dist ((S2 . (n + k)),(S2 . n))) < r;

      let r;

      assume 0 < r;

      then

      consider p such that

       A5: for n, k st p <= n holds ( dist ((S2 . (n + k)),(S2 . n))) < r by A4;

      take p;

      let n, m such that

       A6: p <= n and

       A7: p <= m;

      per cases ;

        suppose n <= m;

        then

        consider k be Nat such that

         A8: m = (n + k) by NAT_1: 10;

        reconsider m9 = m, n9 = n, k as Nat;

        m = (n + k) by A8;

        then ( dist ((S2 . m9),(S2 . n9))) < r by A5, A6;

        hence thesis;

      end;

        suppose m <= n;

        then

        consider k be Nat such that

         A9: n = (m + k) by NAT_1: 10;

        reconsider k as Nat;

        n = (m + k) by A9;

        hence thesis by A5, A7;

      end;

    end;

    theorem :: TBSP_1:7

    for f be Contraction of M st M is complete holds ex c st (f . c) = c & for y be Element of M st (f . y) = y holds y = c

    proof

      let f be Contraction of M;

      consider L such that

       A1: 0 < L and

       A2: L < 1 and

       A3: for x,y be Point of M holds ( dist ((f . x),(f . y))) <= (L * ( dist (x,y))) by ALI2:def 1;

      

       A4: (1 - L) > 0 by A2, XREAL_1: 50;

      ex S1 st for n holds (S1 . (n + 1)) = (f . (S1 . n))

      proof

        set z = the Element of M;

        deffunc U( Nat, Element of M) = (f . $2);

        ex h be sequence of the carrier of M st (h . 0 ) = z & for n be Nat holds (h . (n + 1)) = U(n,.) from NAT_1:sch 12;

        then

        consider h be sequence of the carrier of M such that (h . 0 ) = z and

         A5: for n be Nat holds (h . (n + 1)) = (f . (h . n));

        take h;

        let n;

        thus thesis by A5;

      end;

      then

      consider S1 such that

       A6: for n holds (S1 . (n + 1)) = (f . (S1 . n));

      set r = ( dist ((S1 . 1),(S1 . 0 )));

      

       A7: 0 <= r by METRIC_1: 5;

      

       A8: (1 - L) <> 0 by A2;

      assume

       A9: M is complete;

      now

        per cases ;

          suppose

           A10: 0 = r;

          

           A11: (f . (S1 . 0 )) = (S1 . ( 0 + 1)) by A6

          .= (S1 . 0 ) by A10, METRIC_1: 2;

          for y be Element of M st (f . y) = y holds y = (S1 . 0 )

          proof

            let y be Element of M;

            assume

             A12: (f . y) = y;

            

             A13: ( dist (y,(S1 . 0 ))) >= 0 by METRIC_1: 5;

            assume y <> (S1 . 0 );

            then ( dist (y,(S1 . 0 ))) <> 0 by METRIC_1: 2;

            then (L * ( dist (y,(S1 . 0 )))) < ( dist (y,(S1 . 0 ))) by A2, A13, XREAL_1: 157;

            hence contradiction by A3, A11, A12;

          end;

          hence thesis by A11;

        end;

          suppose

           A14: 0 <> r;

          

           A15: for n holds ( dist ((S1 . (n + 1)),(S1 . n))) <= (r * (L to_power n))

          proof

            defpred X[ Nat] means ( dist ((S1 . ($1 + 1)),(S1 . $1))) <= (r * (L to_power $1));

            

             A16: for k st X[k] holds X[(k + 1)]

            proof

              let k be Nat;

              assume ( dist ((S1 . (k + 1)),(S1 . k))) <= (r * (L to_power k));

              then

               A17: (L * ( dist ((S1 . (k + 1)),(S1 . k)))) <= (L * (r * (L to_power k))) by A1, XREAL_1: 64;

              ( dist ((S1 . ((k + 1) + 1)),(S1 . (k + 1)))) = ( dist ((f . (S1 . (k + 1))),(S1 . (k + 1)))) by A6

              .= ( dist ((f . (S1 . (k + 1))),(f . (S1 . k)))) by A6;

              then

               A18: ( dist ((S1 . ((k + 1) + 1)),(S1 . (k + 1)))) <= (L * ( dist ((S1 . (k + 1)),(S1 . k)))) by A3;

              (L * (r * (L to_power k))) = (r * (L * (L to_power k)))

              .= (r * ((L to_power k) * (L to_power 1))) by POWER: 25

              .= (r * (L to_power (k + 1))) by A1, POWER: 27;

              hence thesis by A18, A17, XXREAL_0: 2;

            end;

            ( dist ((S1 . ( 0 + 1)),(S1 . 0 ))) = (r * 1)

            .= (r * (L to_power 0 )) by POWER: 24;

            then

             A19: X[ 0 ];

            thus for k holds X[k] from NAT_1:sch 2( A19, A16);

          end;

          

           A20: for k holds ( dist ((S1 . k),(S1 . 0 ))) <= (r * ((1 - (L to_power k)) / (1 - L)))

          proof

            defpred X[ Nat] means ( dist ((S1 . $1),(S1 . 0 ))) <= (r * ((1 - (L to_power $1)) / (1 - L)));

            

             A21: for k st X[k] holds X[(k + 1)]

            proof

              let k be Nat such that

               A22: ( dist ((S1 . k),(S1 . 0 ))) <= (r * ((1 - (L to_power k)) / (1 - L)));

              ( dist ((S1 . (k + 1)),(S1 . k))) <= (r * (L to_power k)) by A15;

              then

               A23: ( dist ((S1 . (k + 1)),(S1 . 0 ))) <= (( dist ((S1 . (k + 1)),(S1 . k))) + ( dist ((S1 . k),(S1 . 0 )))) & (( dist ((S1 . (k + 1)),(S1 . k))) + ( dist ((S1 . k),(S1 . 0 )))) <= ((r * (L to_power k)) + (r * ((1 - (L to_power k)) / (1 - L)))) by A22, METRIC_1: 4, XREAL_1: 7;

              ((r * (L to_power k)) + (r * ((1 - (L to_power k)) / (1 - L)))) = (r * ((L to_power k) + ((1 - (L to_power k)) / (1 - L))))

              .= (r * ((((L to_power k) / (1 - L)) * (1 - L)) + ((1 - (L to_power k)) / (1 - L)))) by A8, XCMPLX_1: 87

              .= (r * ((((1 - L) * (L to_power k)) / (1 - L)) + ((1 - (L to_power k)) / (1 - L)))) by XCMPLX_1: 74

              .= (r * ((((1 * (L to_power k)) - (L * (L to_power k))) + (1 - (L to_power k))) / (1 - L))) by XCMPLX_1: 62

              .= (r * ((1 - (L * (L to_power k))) / (1 - L)))

              .= (r * ((1 - ((L to_power k) * (L to_power 1))) / (1 - L))) by POWER: 25

              .= (r * ((1 - (L to_power (k + 1))) / (1 - L))) by A1, POWER: 27;

              hence thesis by A23, XXREAL_0: 2;

            end;

            (r * ((1 - (L to_power 0 )) / (1 - L))) = (r * ((1 - 1) / (1 - L))) by POWER: 24

            .= 0 ;

            then

             A24: X[ 0 ] by METRIC_1: 1;

            thus for k holds X[k] from NAT_1:sch 2( A24, A21);

          end;

          

           A25: for k holds ( dist ((S1 . k),(S1 . 0 ))) <= (r / (1 - L))

          proof

            let k be Nat;

             0 < (L to_power k) by A1, A2, Th2;

            then (1 - (L to_power k)) <= 1 by XREAL_1: 44;

            then ((1 - (L to_power k)) / (1 - L)) <= (1 / (1 - L)) by A4, XREAL_1: 72;

            then

             A26: (r * ((1 - (L to_power k)) / (1 - L))) <= (r * (1 / (1 - L))) by A7, XREAL_1: 64;

            ( dist ((S1 . k),(S1 . 0 ))) <= (r * ((1 - (L to_power k)) / (1 - L))) by A20;

            then ( dist ((S1 . k),(S1 . 0 ))) <= (r * (1 / (1 - L))) by A26, XXREAL_0: 2;

            hence thesis by XCMPLX_1: 99;

          end;

          

           A27: for n, k holds ( dist ((S1 . (n + k)),(S1 . n))) <= ((L to_power n) * ( dist ((S1 . k),(S1 . 0 ))))

          proof

            defpred X[ Nat] means for k holds ( dist ((S1 . ($1 + k)),(S1 . $1))) <= ((L to_power $1) * ( dist ((S1 . k),(S1 . 0 ))));

            

             A28: for n st X[n] holds X[(n + 1)]

            proof

              let n such that

               A29: for k holds ( dist ((S1 . (n + k)),(S1 . n))) <= ((L to_power n) * ( dist ((S1 . k),(S1 . 0 ))));

              let k be Nat;

              

               A30: (L * ((L to_power n) * ( dist ((S1 . k),(S1 . 0 ))))) = ((L * (L to_power n)) * ( dist ((S1 . k),(S1 . 0 ))))

              .= (((L to_power n) * (L to_power 1)) * ( dist ((S1 . k),(S1 . 0 )))) by POWER: 25

              .= ((L to_power (n + 1)) * ( dist ((S1 . k),(S1 . 0 )))) by A1, POWER: 27;

              ( dist ((S1 . ((n + 1) + k)),(S1 . (n + 1)))) = ( dist ((S1 . ((n + k) + 1)),(S1 . (n + 1))))

              .= ( dist ((f . (S1 . (n + k))),(S1 . (n + 1)))) by A6

              .= ( dist ((f . (S1 . (n + k))),(f . (S1 . n)))) by A6;

              then

               A31: ( dist ((S1 . ((n + 1) + k)),(S1 . (n + 1)))) <= (L * ( dist ((S1 . (n + k)),(S1 . n)))) by A3;

              (L * ( dist ((S1 . (n + k)),(S1 . n)))) <= (L * ((L to_power n) * ( dist ((S1 . k),(S1 . 0 ))))) by A1, A29, XREAL_1: 64;

              hence thesis by A31, A30, XXREAL_0: 2;

            end;

            

             A32: X[ 0 ]

            proof

              let n;

              ((L to_power 0 ) * ( dist ((S1 . n),(S1 . 0 )))) = (1 * ( dist ((S1 . n),(S1 . 0 )))) by POWER: 24

              .= ( dist ((S1 . n),(S1 . 0 )));

              hence thesis;

            end;

            thus for k holds X[k] from NAT_1:sch 2( A32, A28);

          end;

          

           A33: for n, k holds ( dist ((S1 . (n + k)),(S1 . n))) <= ((r / (1 - L)) * (L to_power n))

          proof

            let n,k be Nat;

             0 <= (L to_power n) by A1, A2, Th2;

            then

             A34: ((L to_power n) * ( dist ((S1 . k),(S1 . 0 )))) <= ((L to_power n) * (r / (1 - L))) by A25, XREAL_1: 64;

            ( dist ((S1 . (n + k)),(S1 . n))) <= ((L to_power n) * ( dist ((S1 . k),(S1 . 0 )))) by A27;

            hence thesis by A34, XXREAL_0: 2;

          end;

          for s st s > 0 holds ex p st for n, k st p <= n holds ( dist ((S1 . (n + k)),(S1 . n))) < s

          proof

            

             A35: ((1 - L) / r) > 0 by A4, A7, A14, XREAL_1: 139;

            let s;

            assume s > 0 ;

            then (((1 - L) / r) * s) > 0 by A35, XREAL_1: 129;

            then

            consider p such that

             A36: (L to_power p) < (((1 - L) / r) * s) by A1, A2, Th3;

            take p;

            let n,k be Nat;

            assume p <= n;

            then (L to_power n) <= (L to_power p) by A1, A2, Th1;

            then

             A37: (L to_power n) < (((1 - L) / r) * s) by A36, XXREAL_0: 2;

            (r / (1 - L)) > 0 by A4, A7, A14, XREAL_1: 139;

            then

             A38: ((r / (1 - L)) * (L to_power n)) < ((r / (1 - L)) * (((1 - L) / r) * s)) by A37, XREAL_1: 68;

            

             A39: ( dist ((S1 . (n + k)),(S1 . n))) <= ((r / (1 - L)) * (L to_power n)) by A33;

            ((r / (1 - L)) * (((1 - L) / r) * s)) = (((r / (1 - L)) * ((1 - L) / r)) * s)

            .= (((r * (1 - L)) / (r * (1 - L))) * s) by XCMPLX_1: 76

            .= (1 * s) by A8, A14, XCMPLX_1: 6, XCMPLX_1: 60

            .= s;

            hence thesis by A38, A39, XXREAL_0: 2;

          end;

          then S1 is Cauchy by Th6;

          then S1 is convergent by A9;

          then

          consider x be Element of M such that

           A40: for r st r > 0 holds ex n st for m st n <= m holds ( dist ((S1 . m),x)) < r;

          

           A41: (f . x) = x

          proof

            set a = (( dist (x,(f . x))) / 4);

            assume x <> (f . x);

            then

             A42: ( dist (x,(f . x))) <> 0 by METRIC_1: 2;

            

             A43: ( dist (x,(f . x))) >= 0 by METRIC_1: 5;

            then

            consider n such that

             A44: for m st n <= m holds ( dist ((S1 . m),x)) < a by A40, A42, XREAL_1: 224;

            ( dist ((S1 . (n + 1)),(f . x))) = ( dist ((f . (S1 . n)),(f . x))) by A6;

            then

             A45: ( dist ((S1 . (n + 1)),(f . x))) <= (L * ( dist ((S1 . n),x))) by A3;

            

             A46: ( dist ((S1 . n),x)) < a by A44;

            (L * ( dist ((S1 . n),x))) <= ( dist ((S1 . n),x)) by A2, METRIC_1: 5, XREAL_1: 153;

            then ( dist ((S1 . (n + 1)),(f . x))) <= ( dist ((S1 . n),x)) by A45, XXREAL_0: 2;

            then

             A47: ( dist ((S1 . (n + 1)),(f . x))) < a by A46, XXREAL_0: 2;

            

             A48: ( dist (x,(f . x))) <= (( dist (x,(S1 . (n + 1)))) + ( dist ((S1 . (n + 1)),(f . x)))) & (( dist (x,(f . x))) / 2) < ( dist (x,(f . x))) by A42, A43, METRIC_1: 4, XREAL_1: 216;

            ( dist (x,(S1 . (n + 1)))) < a by A44, NAT_1: 11;

            then (( dist (x,(S1 . (n + 1)))) + ( dist ((S1 . (n + 1)),(f . x)))) < (a + a) by A47, XREAL_1: 8;

            hence contradiction by A48, XXREAL_0: 2;

          end;

          for y be Element of M st (f . y) = y holds y = x

          proof

            let y be Element of M;

            assume

             A49: (f . y) = y;

            

             A50: ( dist (y,x)) >= 0 by METRIC_1: 5;

            assume y <> x;

            then ( dist (y,x)) <> 0 by METRIC_1: 2;

            then (L * ( dist (y,x))) < ( dist (y,x)) by A2, A50, XREAL_1: 157;

            hence contradiction by A3, A41, A49;

          end;

          hence thesis by A41;

        end;

      end;

      hence thesis;

    end;

    theorem :: TBSP_1:8

    ( TopSpaceMetr T) is compact implies T is complete

    proof

      set TM = ( TopSpaceMetr T);

      

       A1: TM = TopStruct (# the carrier of T, ( Family_open_set T) #) by PCOMPS_1:def 5;

      assume

       A2: ( TopSpaceMetr T) is compact;

      let S2 be sequence of T such that

       A3: S2 is Cauchy;

      S2 is convergent

      proof

        

         A4: for p holds { x where x be Point of T : ex n st p <= n & x = (S2 . n) } <> {}

        proof

          let p be Nat;

          (S2 . p) in { x where x be Point of T : ex n st p <= n & x = (S2 . n) };

          hence thesis;

        end;

        defpred X[ Subset of ( TopSpaceMetr T)] means ex p st $1 = { x where x be Point of T : ex n st p <= n & x = (S2 . n) };

        consider F be Subset-Family of ( TopSpaceMetr T) such that

         A5: for B be Subset of ( TopSpaceMetr T) holds B in F iff X[B] from SUBSET_1:sch 3;

        defpred X[ Point of T] means ex n st 0 <= n & $1 = (S2 . n);

        set B0 = { x where x be Point of T : X[x] };

        

         A6: B0 is Subset of T from DOMAIN_1:sch 7;

        then

         A7: B0 in F by A1, A5;

        reconsider B0 as Subset of ( TopSpaceMetr T) by A1, A6;

        reconsider F as Subset-Family of ( TopSpaceMetr T);

        set G = ( clf F);

        

         A8: ( Cl B0) in G by A7, PCOMPS_1:def 2;

        

         A9: G is centered

        proof

          thus G <> {} by A8;

          let H be set such that

           A10: H <> {} and

           A11: H c= G and

           A12: H is finite;

          

           A13: H c= ( bool the carrier of TM) by A11, XBOOLE_1: 1;

          H is c=-linear

          proof

            let B,C be set;

            assume that

             A14: B in H and

             A15: C in H;

            reconsider B, C as Subset of TM by A13, A14, A15;

            consider V be Subset of TM such that

             A16: B = ( Cl V) and

             A17: V in F by A11, A14, PCOMPS_1:def 2;

            consider p such that

             A18: V = { x where x be Point of T : ex n st p <= n & x = (S2 . n) } by A5, A17;

            consider W be Subset of TM such that

             A19: C = ( Cl W) and

             A20: W in F by A11, A15, PCOMPS_1:def 2;

            consider q be Nat such that

             A21: W = { x where x be Point of T : ex n st q <= n & x = (S2 . n) } by A5, A20;

            now

              per cases ;

                case

                 A22: q <= p;

                thus V c= W

                proof

                  let y be object;

                  assume y in V;

                  then

                  consider x be Point of T such that

                   A23: y = x and

                   A24: ex n st p <= n & x = (S2 . n) by A18;

                  consider n such that

                   A25: p <= n and

                   A26: x = (S2 . n) by A24;

                  q <= n by A22, A25, XXREAL_0: 2;

                  hence thesis by A21, A23, A26;

                end;

              end;

                case

                 A27: p <= q;

                thus W c= V

                proof

                  let y be object;

                  assume y in W;

                  then

                  consider x be Point of T such that

                   A28: y = x and

                   A29: ex n st q <= n & x = (S2 . n) by A21;

                  consider n such that

                   A30: q <= n and

                   A31: x = (S2 . n) by A29;

                  p <= n by A27, A30, XXREAL_0: 2;

                  hence thesis by A18, A28, A31;

                end;

              end;

            end;

            then B c= C or C c= B by A16, A19, PRE_TOPC: 19;

            hence thesis;

          end;

          then

          consider m be set such that

           A32: m in H and

           A33: for C be set st C in H holds m c= C by A10, A12, FINSET_1: 11;

          

           A34: m c= ( meet H) by A10, A33, SETFAM_1: 5;

          reconsider m as Subset of TM by A13, A32;

          consider A be Subset of TM such that

           A35: m = ( Cl A) and

           A36: A in F by A11, A32, PCOMPS_1:def 2;

          A <> {} by A5, A4, A36;

          then m <> {} by A35, PRE_TOPC: 18, XBOOLE_1: 3;

          hence thesis by A34;

        end;

        G is closed by PCOMPS_1: 11;

        then ( meet G) <> {} by A2, A9, COMPTS_1: 4;

        then

        consider c be Point of TM such that

         A37: c in ( meet G) by SUBSET_1: 4;

        reconsider c as Point of T by A1;

        take c;

        let r;

        assume 0 < r;

        then

         A38: 0 < (r / 2) by XREAL_1: 215;

        then

        consider p such that

         A39: for n, m st p <= n & p <= m holds ( dist ((S2 . n),(S2 . m))) < (r / 2) by A3;

        ( dist (c,c)) < (r / 2) by A38, METRIC_1: 1;

        then

         A40: c in ( Ball (c,(r / 2))) by METRIC_1: 11;

        reconsider Z = ( Ball (c,(r / 2))) as Subset of ( TopSpaceMetr T) by A1;

        ( Ball (c,(r / 2))) in ( Family_open_set T) by PCOMPS_1: 29;

        then

         A41: Z is open by A1, PRE_TOPC:def 2;

        defpred X[ set] means ex n st p <= n & $1 = (S2 . n);

        set B = { x where x be Point of T : X[x] };

        

         A42: B is Subset of T from DOMAIN_1:sch 7;

        then

         A43: B in F by A1, A5;

        reconsider B as Subset of ( TopSpaceMetr T) by A1, A42;

        ( Cl B) in G by A43, PCOMPS_1:def 2;

        then c in ( Cl B) by A37, SETFAM_1:def 1;

        then B meets Z by A40, A41, PRE_TOPC:def 7;

        then

        consider g be object such that

         A44: g in (B /\ Z) by XBOOLE_0: 4;

        take p;

        let m;

        

         A45: g in B by A44, XBOOLE_0:def 4;

        

         A46: g in Z by A44, XBOOLE_0:def 4;

        then

        reconsider g as Point of T;

        consider x be Point of T such that

         A47: g = x and

         A48: ex n st p <= n & x = (S2 . n) by A45;

        consider n such that

         A49: p <= n and

         A50: x = (S2 . n) by A48;

        assume p <= m;

        then

         A51: ( dist ((S2 . m),(S2 . n))) < (r / 2) by A39, A49;

        ( dist ((S2 . n),c)) < (r / 2) by A46, A47, A50, METRIC_1: 11;

        then

         A52: (( dist ((S2 . m),(S2 . n))) + ( dist ((S2 . n),c))) < ((r / 2) + (r / 2)) by A51, XREAL_1: 8;

        ( dist ((S2 . m),c)) <= (( dist ((S2 . m),(S2 . n))) + ( dist ((S2 . n),c))) by METRIC_1: 4;

        hence thesis by A52, XXREAL_0: 2;

      end;

      hence thesis;

    end;

    theorem :: TBSP_1:9

    N is Reflexive triangle & ( TopSpaceMetr N) is compact implies N is totally_bounded

    proof

      assume

       A1: N is Reflexive;

      set TM = ( TopSpaceMetr N);

      assume

       A2: N is triangle;

      assume

       A3: ( TopSpaceMetr N) is compact;

      let r such that

       A4: r > 0 ;

      defpred X[ Subset of N] means ex x be Element of N st $1 = ( Ball (x,r));

      consider G be Subset-Family of N such that

       A5: for C holds C in G iff X[C] from SUBSET_1:sch 3;

      

       A6: TM = TopStruct (# the carrier of N, ( Family_open_set N) #) by PCOMPS_1:def 5;

      then

      reconsider G as Subset-Family of ( TopSpaceMetr N);

      for x be Element of TM holds x in ( union G)

      proof

        let x be Element of TM;

        reconsider x as Element of N by A6;

        ( dist (x,x)) = 0 by A1, METRIC_1: 1;

        then

         A7: x in ( Ball (x,r)) by A4, METRIC_1: 11;

        ( Ball (x,r)) in G by A5;

        hence thesis by A7, TARSKI:def 4;

      end;

      then ( [#] TM) = ( union G) by SUBSET_1: 28;

      then

       A8: G is Cover of TM by SETFAM_1: 45;

      for C be Subset of ( TopSpaceMetr N) st C in G holds C is open

      proof

        let C be Subset of ( TopSpaceMetr N) such that

         A9: C in G;

        reconsider C as Subset of N by A6;

        ex x be Element of N st C = ( Ball (x,r)) by A5, A9;

        then C in the topology of TM by A2, A6, PCOMPS_1: 29;

        hence thesis by PRE_TOPC:def 2;

      end;

      then G is open by TOPS_2:def 1;

      then

      consider H be Subset-Family of TM such that

       A10: H c= G and

       A11: H is Cover of TM and

       A12: H is finite by A3, A8, COMPTS_1:def 1;

      reconsider H as Subset-Family of N by A6;

      take H;

      ( union H) = the carrier of TM by A11, SETFAM_1: 45;

      hence thesis by A6, A5, A10, A12;

    end;

    definition

      let N be non empty MetrStruct;

      :: TBSP_1:def6

      attr N is bounded means ex r st 0 < r & for x,y be Point of N holds ( dist (x,y)) <= r;

      let C be Subset of N;

      :: TBSP_1:def7

      attr C is bounded means ex r st 0 < r & for x,y be Point of N st x in C & y in C holds ( dist (x,y)) <= r;

    end

    registration

      let A be non empty set;

      cluster ( DiscreteSpace A) -> bounded;

      coherence

      proof

        take 2;

        set N = ( DiscreteSpace A);

        thus 0 < 2;

        let x,y be Point of N;

        

         A1: N = MetrStruct (# A, ( discrete_dist A) #) & ( dist (x,y)) = (the distance of N . (x,y)) by METRIC_1:def 1, METRIC_1:def 11;

        x = y or x <> y;

        then ( dist (x,y)) = 0 or ( dist (x,y)) = 1 by A1, METRIC_1:def 10;

        hence ( dist (x,y)) <= 2;

      end;

    end

    registration

      cluster bounded for non empty MetrSpace;

      existence

      proof

        take ( DiscreteSpace { 0 });

        thus thesis;

      end;

    end

    registration

      let N;

      cluster empty -> bounded for Subset of N;

      coherence

      proof

        let S be Subset of N;

        assume

         A1: S is empty;

        take 1;

        thus thesis by A1;

      end;

    end

    registration

      let N;

      cluster bounded for Subset of N;

      existence

      proof

        take ( {} N);

        thus thesis;

      end;

    end

    theorem :: TBSP_1:10

    

     Th10: for C be Subset of N holds (C <> {} & C is bounded implies ex r, w st 0 < r & w in C & for z be Point of N st z in C holds ( dist (w,z)) <= r) & (N is symmetric triangle & (ex r, w st 0 < r & for z be Point of N st z in C holds ( dist (w,z)) <= r) implies C is bounded)

    proof

      let C be Subset of N;

      thus C <> {} & C is bounded implies ex r, w st 0 < r & w in C & for z be Point of N st z in C holds ( dist (w,z)) <= r

      proof

        set w = the Element of C;

        assume

         A1: C <> {} ;

        then

        reconsider w as Point of N by TARSKI:def 3;

        assume C is bounded;

        then

        consider r such that

         A2: 0 < r and

         A3: for x,y be Point of N st x in C & y in C holds ( dist (x,y)) <= r;

        take r;

        take w;

        thus 0 < r by A2;

        thus w in C by A1;

        let z be Point of N;

        assume z in C;

        hence thesis by A3;

      end;

      assume

       A4: N is symmetric;

      assume

       A5: N is triangle;

      given r, w such that

       A6: 0 < r and

       A7: for z be Point of N st z in C holds ( dist (w,z)) <= r;

      set s = (r + r);

      reconsider N as symmetric MetrStruct by A4;

      reconsider w as Element of N;

      ex s st 0 < s & for x,y be Point of N st x in C & y in C holds ( dist (x,y)) <= s

      proof

        take s;

        thus 0 < s by A6;

        let x,y be Point of N;

        assume that

         A8: x in C and

         A9: y in C;

        

         A10: ( dist (w,x)) <= r by A7, A8;

        ( dist (w,y)) <= r by A7, A9;

        then

         A11: (( dist (x,w)) + ( dist (w,y))) <= s by A10, XREAL_1: 7;

        ( dist (x,y)) <= (( dist (x,w)) + ( dist (w,y))) by A5, METRIC_1: 4;

        hence thesis by A11, XXREAL_0: 2;

      end;

      hence thesis;

    end;

    theorem :: TBSP_1:11

    

     Th11: for r be Real holds N is Reflexive & 0 < r implies w in ( Ball (w,r))

    proof

      let r be Real;

      assume N is Reflexive;

      then

       A1: ( dist (w,w)) = 0 by METRIC_1: 1;

      assume 0 < r;

      hence thesis by A1, METRIC_1: 11;

    end;

    theorem :: TBSP_1:12

    

     Th12: for r be Real holds r <= 0 implies ( Ball (t1,r)) = {}

    proof

      let r be Real;

      assume

       A1: r <= 0 ;

      set c = the Element of ( Ball (t1,r));

      assume

       A2: ( Ball (t1,r)) <> {} ;

      then

      reconsider c as Point of T by TARSKI:def 3;

      ( dist (t1,c)) < r by A2, METRIC_1: 11;

      hence contradiction by A1, METRIC_1: 5;

    end;

    

     Lm2: for r be Real holds 0 < r implies ( Ball (t1,r)) is bounded

    proof

      let r be Real;

      assume

       A1: 0 < r;

      set P = ( Ball (t1,r));

      reconsider r as Real;

      ex r, t1 st 0 < r & t1 in P & for z be Point of T st z in P holds ( dist (t1,z)) <= r

      proof

        take r, t1;

        thus 0 < r by A1;

        thus t1 in P by A1, Th11;

        let z be Point of T;

        assume z in P;

        hence thesis by METRIC_1: 11;

      end;

      hence thesis by Th10;

    end;

    registration

      let T, t1;

      let r be Real;

      cluster ( Ball (t1,r)) -> bounded;

      coherence

      proof

        per cases ;

          suppose r <= 0 ;

          then ( Ball (t1,r)) = ( {} T) by Th12;

          hence thesis;

        end;

          suppose 0 < r;

          hence thesis by Lm2;

        end;

      end;

    end

    theorem :: TBSP_1:13

    

     Th13: for P,Q be Subset of T holds P is bounded & Q is bounded implies (P \/ Q) is bounded

    proof

      let P,Q be Subset of T;

      assume that

       A1: P is bounded and

       A2: Q is bounded;

      per cases ;

        suppose P = {} ;

        hence thesis by A2;

      end;

        suppose

         A3: P <> {} ;

        now

          per cases ;

            suppose Q = {} ;

            hence thesis by A1;

          end;

            suppose Q <> {} ;

            then

            consider s be Real, d be Element of T such that

             A4: 0 < s and d in Q and

             A5: for z be Point of T st z in Q holds ( dist (d,z)) <= s by A2, Th10;

            consider r, t1 such that

             A6: 0 < r and

             A7: t1 in P and

             A8: for z be Point of T st z in P holds ( dist (t1,z)) <= r by A1, A3, Th10;

            set t = ((r + s) + ( dist (t1,d)));

            

             A9: 0 <= ( dist (t1,d)) by METRIC_1: 5;

            then

             A10: r < (r + (( dist (t1,d)) + s)) by A4, XREAL_1: 29;

            ex t be Real, t1 st 0 < t & t1 in (P \/ Q) & for z be Point of T st z in (P \/ Q) holds ( dist (t1,z)) <= t

            proof

              reconsider t as Real;

              take t, t1;

              thus 0 < t by A6, A4, A9;

              thus t1 in (P \/ Q) by A7, XBOOLE_0:def 3;

              let z be Point of T;

              assume z in (P \/ Q);

              then

               A11: z in P or z in Q by XBOOLE_0:def 3;

              now

                per cases by A8, A5, A11;

                  suppose ( dist (t1,z)) <= r;

                  hence thesis by A10, XXREAL_0: 2;

                end;

                  suppose ( dist (d,z)) <= s;

                  then ( dist (t1,z)) <= (( dist (t1,d)) + ( dist (d,z))) & (( dist (t1,d)) + ( dist (d,z))) <= (( dist (t1,d)) + s) by METRIC_1: 4, XREAL_1: 7;

                  then

                   A12: ( dist (t1,z)) <= (( dist (t1,d)) + s) by XXREAL_0: 2;

                  (( dist (t1,d)) + s) <= (r + (( dist (t1,d)) + s)) by A6, XREAL_1: 29;

                  hence thesis by A12, XXREAL_0: 2;

                end;

              end;

              hence thesis;

            end;

            hence thesis by Th10;

          end;

        end;

        hence thesis;

      end;

    end;

    theorem :: TBSP_1:14

    

     Th14: for C,D be Subset of N holds C is bounded & D c= C implies D is bounded

    proof

      let C,D be Subset of N;

      assume that

       A1: C is bounded and

       A2: D c= C;

      consider r such that

       A3: 0 < r and

       A4: for x,y be Point of N st x in C & y in C holds ( dist (x,y)) <= r by A1;

      ex r st 0 < r & for x,y be Point of N st x in D & y in D holds ( dist (x,y)) <= r

      proof

        take r;

        thus 0 < r by A3;

        let x,y be Point of N;

        assume x in D & y in D;

        hence thesis by A2, A4;

      end;

      hence thesis;

    end;

    theorem :: TBSP_1:15

    

     Th15: for P be Subset of T holds P = {t1} implies P is bounded

    proof

      let P be Subset of T;

      assume

       A1: P = {t1};

       {t1} is Subset of ( Ball (t1,1)) by Th11, SUBSET_1: 41;

      hence thesis by A1, Th14;

    end;

    theorem :: TBSP_1:16

    

     Th16: for P be Subset of T holds P is finite implies P is bounded

    proof

      let P be Subset of T;

      defpred P[ set] means ex X be Subset of T st X = $1 & X is bounded;

      ( {} T) is bounded;

      then

       A1: P[ {} ];

      

       A2: for x,B be set st x in P & B c= P & P[B] holds P[(B \/ {x})]

      proof

        let x,B be set such that

         A3: x in P and B c= P and

         A4: P[B];

        reconsider x as Element of T by A3;

        reconsider W = {x} as Subset of T;

        consider X be Subset of T such that

         A5: X = B & X is bounded by A4;

        

         A6: W is bounded by Th15;

        ex Y be Subset of T st Y = (B \/ {x}) & Y is bounded

        proof

          take (X \/ W);

          thus thesis by A5, A6, Th13;

        end;

        hence thesis;

      end;

      assume

       A7: P is finite;

       P[P] from FINSET_1:sch 2( A7, A1, A2);

      hence thesis;

    end;

    registration

      let T;

      cluster finite -> bounded for Subset of T;

      coherence by Th16;

    end

    registration

      let T;

      cluster finite non empty for Subset of T;

      existence

      proof

        take the finite non empty Subset of T;

        thus thesis;

      end;

    end

    theorem :: TBSP_1:17

    

     Th17: Y is finite & (for P be Subset of T st P in Y holds P is bounded) implies ( union Y) is bounded

    proof

      assume that

       A1: Y is finite and

       A2: for P be Subset of T st P in Y holds P is bounded;

      defpred P[ set] means ex X be Subset of T st X = ( union $1) & X is bounded;

      

       A3: for x,B be set st x in Y & B c= Y & P[B] holds P[(B \/ {x})]

      proof

        let x,B be set such that

         A4: x in Y and B c= Y and

         A5: P[B];

        consider X be Subset of T such that

         A6: X = ( union B) & X is bounded by A5;

        reconsider x as Subset of T by A4;

        

         A7: ( union (B \/ {x})) = (( union B) \/ ( union {x})) by ZFMISC_1: 78

        .= (( union B) \/ x) by ZFMISC_1: 25;

        

         A8: x is bounded by A2, A4;

        ex Y be Subset of T st Y = ( union (B \/ {x})) & Y is bounded

        proof

          take (X \/ x);

          thus thesis by A6, A7, A8, Th13;

        end;

        hence thesis;

      end;

      

       A9: P[ {} ]

      proof

        set m = ( {} T);

        m = ( union {} ) by ZFMISC_1: 2;

        hence thesis;

      end;

       P[Y] from FINSET_1:sch 2( A1, A9, A3);

      hence thesis;

    end;

    theorem :: TBSP_1:18

    

     Th18: N is bounded iff ( [#] N) is bounded

    proof

      thus N is bounded implies ( [#] N) is bounded

      proof

        assume N is bounded;

        then

        consider r such that

         A1: 0 < r and

         A2: for x,y be Point of N holds ( dist (x,y)) <= r;

        for x,y be Point of N st x in ( [#] N) & y in ( [#] N) holds ( dist (x,y)) <= r by A2;

        hence thesis by A1;

      end;

      assume ( [#] N) is bounded;

      then

      consider r such that

       A3: 0 < r and

       A4: for x,y be Point of N st x in ( [#] N) & y in ( [#] N) holds ( dist (x,y)) <= r;

      take r;

      thus 0 < r by A3;

      let x,y be Point of N;

      thus thesis by A4;

    end;

    registration

      let N be bounded non empty MetrStruct;

      cluster ( [#] N) -> bounded;

      coherence by Th18;

    end

    theorem :: TBSP_1:19

    T is totally_bounded implies T is bounded

    proof

      assume T is totally_bounded;

      then

      consider Y such that

       A1: Y is finite & the carrier of T = ( union Y) and

       A2: for P st P in Y holds ex x be Element of T st P = ( Ball (x,1));

      for P be Subset of T st P in Y holds P is bounded

      proof

        let P be Subset of T;

        assume P in Y;

        then ex x be Element of T st P = ( Ball (x,1)) by A2;

        hence thesis;

      end;

      then ( [#] T) is bounded by A1, Th17;

      hence thesis by Th18;

    end;

    definition

      let N be Reflexive non empty MetrStruct, C be Subset of N;

      assume

       A1: C is bounded;

      :: TBSP_1:def8

      func diameter C -> Real means

      : Def8: (for x,y be Point of N st x in C & y in C holds ( dist (x,y)) <= it ) & for s st (for x,y be Point of N st x in C & y in C holds ( dist (x,y)) <= s) holds it <= s if C <> {}

      otherwise it = 0 ;

      consistency ;

      existence

      proof

        thus C <> {} implies ex r be Real st (for x,y be Point of N st x in C & y in C holds ( dist (x,y)) <= r) & for s st for x,y be Point of N st x in C & y in C holds ( dist (x,y)) <= s holds r <= s

        proof

          set c = the Element of C;

          defpred X[ Real] means for x,y be Point of N st x in C & y in C holds ( dist (x,y)) <= $1;

          set I = { r where r be Element of REAL : X[r] };

          defpred X[ set] means ex x,y be Point of N st x in C & y in C & $1 = ( dist (x,y));

          set J = { r where r be Element of REAL : X[r] };

          

           A2: for a,b be Real st a in J & b in I holds a <= b

          proof

            let a,b be Real;

            assume a in J & b in I;

            then (ex t be Element of REAL st t = a & ex x,y be Point of N st x in C & y in C & t = ( dist (x,y))) & ex t9 be Element of REAL st t9 = b & for x,y be Point of N st x in C & y in C holds ( dist (x,y)) <= t9;

            hence thesis;

          end;

          

           A3: J is Subset of REAL from DOMAIN_1:sch 7;

          assume

           A4: C <> {} ;

          then

          reconsider c as Point of N by TARSKI:def 3;

          ( dist (c,c)) = 0 by METRIC_1: 1;

          then

           A5: ( In ( 0 , REAL )) in J by A4;

          reconsider J as Subset of REAL by A3;

          

           A6: I is Subset of REAL from DOMAIN_1:sch 7;

          consider r such that 0 < r and

           A7: for x,y be Point of N st x in C & y in C holds ( dist (x,y)) <= r by A1;

          reconsider r as Element of REAL by XREAL_0:def 1;

          

           A8: r in I by A7;

          reconsider I as Subset of REAL by A6;

          consider d be Real such that

           A9: for a be Real st a in J holds a <= d and

           A10: for b be Real st b in I holds d <= b by A8, A5, A2, MEMBERED: 37;

          take d;

          thus for x,y be Point of N st x in C & y in C holds ( dist (x,y)) <= d

          proof

            let x,y be Point of N;

            assume

             A11: x in C & y in C;

            ( dist (x,y)) in REAL by XREAL_0:def 1;

            then ( dist (x,y)) in J by A11;

            hence thesis by A9;

          end;

          let s;

          assume

           A12: for x,y be Point of N st x in C & y in C holds ( dist (x,y)) <= s;

          reconsider s as Element of REAL by XREAL_0:def 1;

          s in I by A12;

          hence thesis by A10;

        end;

        thus thesis;

      end;

      uniqueness

      proof

        let r1,r2 be Real;

        hereby

          assume C <> {} ;

          assume (for x,y be Point of N st x in C & y in C holds ( dist (x,y)) <= r1) & ((for s st for x,y be Point of N st x in C & y in C holds ( dist (x,y)) <= s holds r1 <= s) & for x,y be Point of N st x in C & y in C holds ( dist (x,y)) <= r2) & for s st for x,y be Point of N st x in C & y in C holds ( dist (x,y)) <= s holds r2 <= s;

          then r1 <= r2 & r2 <= r1;

          hence r1 = r2 by XXREAL_0: 1;

        end;

        thus thesis;

      end;

    end

    theorem :: TBSP_1:20

    for P be Subset of T holds P = {x} implies ( diameter P) = 0

    proof

      let P be Subset of T;

      assume

       A1: P = {x};

      then

       A2: x in P by TARSKI:def 1;

      then

      reconsider t1 = x as Element of T;

      (for x,y be Point of T st x in P & y in P holds ( dist (x,y)) <= 0 ) & for s st (for x,y be Point of T st x in P & y in P holds ( dist (x,y)) <= s) holds 0 <= s

      proof

        thus for x,y be Point of T st x in P & y in P holds ( dist (x,y)) <= 0

        proof

          let x,y be Point of T such that

           A3: x in P and

           A4: y in P;

          x = t1 by A1, A3, TARSKI:def 1;

          

          then ( dist (x,y)) = ( dist (t1,t1)) by A1, A4, TARSKI:def 1

          .= 0 by METRIC_1: 1;

          hence thesis;

        end;

        let s;

        assume for x,y be Point of T st x in P & y in P holds ( dist (x,y)) <= s;

        then ( dist (t1,t1)) <= s by A2;

        hence thesis by METRIC_1: 1;

      end;

      hence thesis by A1, Def8;

    end;

    theorem :: TBSP_1:21

    

     Th21: for S be Subset of R st S is bounded holds 0 <= ( diameter S)

    proof

      let S be Subset of R;

      assume

       A1: S is bounded;

      per cases ;

        suppose S = {} ;

        hence thesis by Def8;

      end;

        suppose

         A2: S <> {} ;

        set x = the Element of S;

        reconsider x as Element of R by A2, TARSKI:def 3;

        ( dist (x,x)) <= ( diameter S) by A1, A2, Def8;

        hence thesis by METRIC_1: 1;

      end;

    end;

    theorem :: TBSP_1:22

    for A be Subset of M holds A <> {} & A is bounded & ( diameter A) = 0 implies ex g be Point of M st A = {g}

    proof

      let A be Subset of M;

      assume that

       A1: A <> {} and

       A2: A is bounded;

      thus ( diameter A) = 0 implies ex g be Point of M st A = {g}

      proof

        set g = the Element of A;

        reconsider g as Element of M by A1, TARSKI:def 3;

        assume

         A3: ( diameter A) = 0 ;

        reconsider Z = {g} as Subset of M;

        take g;

        for x be Element of M holds x in A iff x in Z

        proof

          let x be Element of M;

          thus x in A implies x in Z

          proof

            assume x in A;

            then ( dist (x,g)) <= 0 by A2, A3, Def8;

            then ( dist (x,g)) = 0 by METRIC_1: 5;

            then x = g by METRIC_1: 2;

            hence thesis by TARSKI:def 1;

          end;

          assume

           A4: x in Z;

          g in A by A1;

          hence thesis by A4, TARSKI:def 1;

        end;

        hence thesis by SUBSET_1: 3;

      end;

    end;

    theorem :: TBSP_1:23

     0 < r implies ( diameter ( Ball (t1,r))) <= (2 * r)

    proof

      

       A1: for x,y be Point of T st x in ( Ball (t1,r)) & y in ( Ball (t1,r)) holds ( dist (x,y)) <= (2 * r)

      proof

        let x,y be Point of T;

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

        then ( dist (t1,x)) < r & ( dist (t1,y)) < r by METRIC_1: 11;

        then

         A2: (( dist (t1,x)) + ( dist (t1,y))) < (r + r) by XREAL_1: 8;

        ( dist (x,y)) <= (( dist (x,t1)) + ( dist (t1,y))) by METRIC_1: 4;

        hence thesis by A2, XXREAL_0: 2;

      end;

      assume 0 < r;

      then t1 in ( Ball (t1,r)) by Th11;

      hence thesis by A1, Def8;

    end;

    theorem :: TBSP_1:24

    for S,V be Subset of R holds S is bounded & V c= S implies ( diameter V) <= ( diameter S)

    proof

      let S,V be Subset of R;

      assume that

       A1: S is bounded and

       A2: V c= S;

      

       A3: V is bounded by A1, A2, Th14;

      per cases ;

        suppose V = {} ;

        then ( diameter V) = 0 by Def8;

        hence thesis by A1, Th21;

      end;

        suppose

         A4: V <> {} ;

        for x,y be Point of R st x in V & y in V holds ( dist (x,y)) <= ( diameter S) by A1, A2, Def8;

        hence thesis by A3, A4, Def8;

      end;

    end;

    theorem :: TBSP_1:25

    for P,Q be Subset of T holds P is bounded & Q is bounded & P meets Q implies ( diameter (P \/ Q)) <= (( diameter P) + ( diameter Q))

    proof

      let P,Q be Subset of T;

      assume that

       A1: P is bounded and

       A2: Q is bounded and

       A3: (P /\ Q) <> {} ;

      set g = the Element of (P /\ Q);

      

       A4: g in Q by A3, XBOOLE_0:def 4;

      set s = (( diameter P) + ( diameter Q));

      set b = ( diameter Q);

      

       A5: b <= s by A1, Th21, XREAL_1: 31;

      set a = ( diameter P);

      

       A6: g in P by A3, XBOOLE_0:def 4;

      reconsider g as Element of T by A3, TARSKI:def 3;

      

       A7: a <= s by A2, Th21, XREAL_1: 31;

      

       A8: for x,y be Point of T st x in (P \/ Q) & y in (P \/ Q) holds ( dist (x,y)) <= s

      proof

        let x,y be Point of T such that

         A9: x in (P \/ Q) and

         A10: y in (P \/ Q);

        

         A11: ( dist (x,y)) <= (( dist (x,g)) + ( dist (g,y))) by METRIC_1: 4;

        now

          per cases by A9, XBOOLE_0:def 3;

            suppose

             A12: x in P;

            now

              per cases by A10, XBOOLE_0:def 3;

                suppose y in P;

                then ( dist (x,y)) <= a by A1, A12, Def8;

                hence thesis by A7, XXREAL_0: 2;

              end;

                suppose

                 A13: y in Q;

                

                 A14: ( dist (x,g)) <= a by A1, A6, A12, Def8;

                ( dist (g,y)) <= b by A2, A4, A13, Def8;

                then (( dist (x,g)) + ( dist (g,y))) <= (a + b) by A14, XREAL_1: 7;

                hence thesis by A11, XXREAL_0: 2;

              end;

            end;

            hence thesis;

          end;

            suppose

             A15: x in Q;

            now

              per cases by A10, XBOOLE_0:def 3;

                suppose

                 A16: y in P;

                

                 A17: ( dist (x,g)) <= b by A2, A4, A15, Def8;

                ( dist (g,y)) <= a by A1, A6, A16, Def8;

                then (( dist (x,g)) + ( dist (g,y))) <= (b + a) by A17, XREAL_1: 7;

                hence thesis by A11, XXREAL_0: 2;

              end;

                suppose y in Q;

                then ( dist (x,y)) <= b by A2, A15, Def8;

                hence thesis by A5, XXREAL_0: 2;

              end;

            end;

            hence thesis;

          end;

        end;

        hence thesis;

      end;

      P <> {} & (P \/ Q) is bounded by A1, A2, A3, Th13;

      hence thesis by A8, Def8;

    end;

    theorem :: TBSP_1:26

    for S1 be sequence of T holds S1 is Cauchy implies ( rng S1) is bounded

    proof

      let S1 be sequence of T;

      set A = ( rng S1);

      assume S1 is Cauchy;

      then

      consider p such that

       A1: for n, m st p <= n & p <= m holds ( dist ((S1 . n),(S1 . m))) < 1;

      defpred X[ set] means ex n st p <= n & $1 = (S1 . n);

      reconsider B = { t1 where t1 be Point of T : X[t1] } as Subset of T from DOMAIN_1:sch 7;

      defpred X[ set] means ex n st n <= p & $1 = (S1 . n);

      reconsider C = { t1 where t1 be Point of T : X[t1] } as Subset of T from DOMAIN_1:sch 7;

      reconsider B, C as Subset of T;

      

       A2: C is finite

      proof

        set K = ( Seg p);

        set J = ( { 0 } \/ K);

        now

          let x be object;

          thus x in C implies x in (S1 .: J)

          proof

            assume x in C;

            then

            consider t1 such that

             A3: x = t1 and

             A4: ex n st n <= p & t1 = (S1 . n);

            consider n such that

             A5: n <= p and

             A6: t1 = (S1 . n) by A4;

            n in NAT by ORDINAL1:def 12;

            then

             A7: n in ( dom S1) by FUNCT_2:def 1;

            now

              per cases by NAT_1: 6;

                suppose n = 0 ;

                then n in { 0 } by TARSKI:def 1;

                then n in J by XBOOLE_0:def 3;

                hence thesis by A3, A6, A7, FUNCT_1:def 6;

              end;

                suppose ex m be Nat st n = (m + 1);

                then 1 <= n by NAT_1: 11;

                then n in { k where k be Nat : 1 <= k & k <= p } by A5;

                then n in K by FINSEQ_1:def 1;

                then n in J by XBOOLE_0:def 3;

                hence thesis by A3, A6, A7, FUNCT_1:def 6;

              end;

            end;

            hence thesis;

          end;

          assume x in (S1 .: J);

          then

          consider y be object such that

           A8: y in ( dom S1) and

           A9: y in J and

           A10: x = (S1 . y) by FUNCT_1:def 6;

          reconsider y as Nat by A8;

          now

            per cases by A9, XBOOLE_0:def 3;

              suppose

               A11: y in { 0 };

              (S1 . y) is Element of T;

              then

              reconsider x9 = x as Element of T by A10;

              y = 0 by A11, TARSKI:def 1;

              then ex n st n <= p & x9 = (S1 . n) by A10;

              hence x in C;

            end;

              suppose

               A12: y in K;

              (S1 . y) is Element of T;

              then

              reconsider x9 = x as Element of T by A10;

              y in { k where k be Nat : 1 <= k & k <= p } by A12, FINSEQ_1:def 1;

              then ex k be Nat st y = k & 1 <= k & k <= p;

              then ex n st n <= p & x9 = (S1 . n) by A10;

              hence x in C;

            end;

          end;

          hence x in C;

        end;

        hence thesis by TARSKI: 2;

      end;

      

       A13: A = (B \/ C)

      proof

        thus A c= (B \/ C)

        proof

          let x be object;

          assume x in A;

          then

          consider y be object such that

           A14: y in ( dom S1) and

           A15: x = (S1 . y) by FUNCT_1:def 3;

          reconsider y as Nat by A14;

          (S1 . y) is Element of T;

          then

          reconsider x9 = x as Element of T by A15;

          per cases ;

            suppose y <= p;

            then ex n st n <= p & x9 = (S1 . n) by A15;

            then x in C;

            hence thesis by XBOOLE_0:def 3;

          end;

            suppose p <= y;

            then ex n st p <= n & x9 = (S1 . n) by A15;

            then x in B;

            hence thesis by XBOOLE_0:def 3;

          end;

        end;

        let x be object;

        assume

         A16: x in (B \/ C);

        per cases by A16, XBOOLE_0:def 3;

          suppose x in B;

          then

          consider t1 such that

           A17: x = t1 and

           A18: ex n st p <= n & t1 = (S1 . n);

          consider n such that p <= n and

           A19: t1 = (S1 . n) by A18;

          n in NAT by ORDINAL1:def 12;

          then n in ( dom S1) by FUNCT_2:def 1;

          hence thesis by A17, A19, FUNCT_1:def 3;

        end;

          suppose x in C;

          then

          consider t1 such that

           A20: x = t1 and

           A21: ex n st n <= p & t1 = (S1 . n);

          consider n such that n <= p and

           A22: t1 = (S1 . n) by A21;

          n in NAT by ORDINAL1:def 12;

          then n in ( dom S1) by FUNCT_2:def 1;

          hence thesis by A20, A22, FUNCT_1:def 3;

        end;

      end;

      B is bounded

      proof

        set x = (S1 . p);

        ex r, t1 st 0 < r & t1 in B & for z be Point of T st z in B holds ( dist (t1,z)) <= r

        proof

          take 1, x;

          thus 0 < 1;

          thus x in B;

          let z be Point of T;

          assume z in B;

          then ex t1 st z = t1 & ex n st p <= n & t1 = (S1 . n);

          hence thesis by A1;

        end;

        hence thesis by Th10;

      end;

      hence thesis by A2, A13, Th13;

    end;