:: Totally Bounded Metric Spaces
::  by Alicia de la Cruz
::
:: Received September 30, 1991
:: Copyright (c) 1991-2012 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NUMBERS, XBOOLE_0, METRIC_1, SUBSET_1, SETFAM_1, RELAT_2,
      FUNCT_1, REAL_1, CARD_1, ARYTM_3, XXREAL_0, POWER, RELAT_1, SEQ_1, SEQ_2,
      ORDINAL2, COMPLEX1, ARYTM_1, FINSET_1, STRUCT_0, TARSKI, NAT_1, BHSP_3,
      REWRITE1, ALI2, PRE_TOPC, PCOMPS_1, RCOMP_1, ZFMISC_1, ORDINAL1,
      XXREAL_2, XREAL_0, MEASURE5, FINSEQ_1, TBSP_1;
 notations TARSKI, XBOOLE_0, SUBSET_1, NUMBERS, XREAL_0, COMPLEX1, REAL_1,
      RELAT_1, ORDINAL1, FUNCT_1, RELSET_1, FINSEQ_1, DOMAIN_1, SETFAM_1,
      FUNCT_2, FINSET_1, NAT_1, STRUCT_0, PRE_TOPC, TOPS_2, SEQ_1, SEQ_2,
      COMPTS_1, METRIC_1, POWER, PCOMPS_1, ALI2, XXREAL_0;
 constructors SETFAM_1, DOMAIN_1, XXREAL_0, REAL_1, NAT_1, COMPLEX1, FINSEQ_1,
      SEQ_2, POWER, TOPS_2, COMPTS_1, PCOMPS_1, ALI2, SEQ_1, VALUED_1,
      RELSET_1, COMSEQ_2;
 registrations XBOOLE_0, SUBSET_1, ORDINAL1, RELSET_1, FINSET_1, NUMBERS,
      XXREAL_0, XREAL_0, NAT_1, MEMBERED, FINSEQ_1, STRUCT_0, METRIC_1,
      PCOMPS_1;
 requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
 definitions COMPTS_1, TARSKI, ORDINAL1, XBOOLE_0, STRUCT_0, FINSET_1;
 theorems METRIC_1, SUBSET_1, FUNCT_1, PCOMPS_1, PRE_TOPC, MEMBERED, TOPS_2,
      TARSKI, COMPTS_1, NAT_1, SEQ_2, ZFMISC_1, POWER, SERIES_1, ABSVALUE,
      FUNCT_2, SETFAM_1, FINSEQ_1, ALI2, RELSET_1, XREAL_0, XBOOLE_0, XBOOLE_1,
      XCMPLX_1, FINSET_1, XREAL_1, XXREAL_0, ORDINAL1, RELAT_1;
 schemes DOMAIN_1, SUBSET_1, NAT_1, SEQ_1, FINSET_1;

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 Element of NAT,
  r,s,L for Real,
  x,y for set;

theorem 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 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[Element of 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 Element of 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 1(A7,A3);
end;

theorem Th3:
  for L st 0<L & L<1 holds for s st 0<s ex n st L to_power n<s
proof
  let L such that
A1: 0<L & L<1;
  let s;
  deffunc U(Element of NAT) = L to_power ($1+1);
  consider rseq being Real_Sequence such that
A2: for n 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 such that
A4: for m st n<=m holds abs(rseq.m-0)<s by A3,SEQ_2:def 7;
  take n+1;
A5: 0<L to_power (n+1) by A1,Th2;
  abs(rseq.n-0) = abs(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;
  attr N is totally_bounded means
  :Def1:
  for r st r>0 ex G st G is finite &
  the carrier of N = union G & for C st C in G 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;
    assume y in rng f;
    then consider x 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 by TARSKI:def 3;
  hence thesis by A3,FUNCT_2:def 1,RELSET_1:4;
end;

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

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

definition
  let M,S1;
  assume
A1: S1 is convergent;
  func lim S1 -> Element of M means
  for r st r>0 ex n st for m st m>=n holds dist(S1.m,it)<r;
  existence by A1,Def2;
  uniqueness
  proof
    given g1,g2 such that
A2: for r st r>0 ex n st for m st n<=m holds dist(S1.m,g1)<r and
A3: for r st r>0 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;
  attr S2 is Cauchy means
  :Def4:
  for r st r>0 ex p st for n,m st p<=n & p<=m holds dist(S2.n,S2.m)<r;
end;

definition
  let N;
  attr N is complete means
  :Def5:
  for S2 st S2 is Cauchy holds S2 is convergent;
end;

definition let N,S2; let n be Element of NAT;
 redefine func S2.n -> Element of N;
 coherence
  proof
   thus S2.n is Element of N;  :: refreshment
  end;
end;

theorem 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 being Element of N such that
A4: for r st 0<r ex n st for m st n<=m holds dist(S2.m,g)<r by A3,Def2;
  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 Element of 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 Th6:
  for N being symmetric non empty MetrStruct, S2 being sequence of N
   holds S2 is Cauchy iff for r st r>0 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 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,Def4;
    take p;
    let n,k be Element of 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 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 Element of NAT by ORDINAL1:def 12;
    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 Element of NAT by ORDINAL1:def 12;
    n = m+k by A9;
    hence thesis by A5,A7;
  end;
end;

theorem
  for f being Contraction of M st M is complete ex c st f.c = c & for y
  being 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 being 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 being Function of NAT,the carrier of M st h.0 = z & for n being
    Nat holds h.(n+1) = U(n,h.n) from NAT_1:sch 12;
    then consider h being Function of NAT,the carrier of M such that
    h.0 = z and
A5: for n being 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 being 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[Element of 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 Element of 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 1(A19,A16);
      end;
A20:  for k holds dist(S1.k,S1.0)<=r*((1-L to_power k)/(1-L))
      proof
        defpred X[Element of 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 Element of 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 1(A24,A21);
      end;
A25:  for k holds dist(S1.k,S1.0)<=r/(1-L)
      proof
        let k be Element of 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[Element of 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 Element of 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 1(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 Element of 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 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 Element of 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,60
          .= s;
        hence thesis by A38,A39,XXREAL_0:2;
      end;
      then S1 is Cauchy by Th6;
      then S1 is convergent by A9,Def5;
      then consider x being Element of M such that
A40:  for r st r>0 ex n st for m st n<=m holds dist(S1.m,x)<r by Def2;
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 being 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
  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 is Point of T : ex n st p<=n & x = S2.n} <> {}
    proof
      let p be Element of NAT;
      (S2.p) in {x where x is 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 is Point
    of T : ex n st p<=n & x = S2.n};
    consider F being Subset-Family of TopSpaceMetr(T) such that
A5: for B being 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 is 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 being 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 is Point of T : ex n st p<=n & x = S2.n} by A5,A17;
        consider W being Subset of TM such that
A19:    C = Cl W and
A20:    W in F by A11,A15,PCOMPS_1:def 2;
        consider q being Element of NAT such that
A21:    W = {x where x is 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 set;
              assume y in V;
              then consider x being 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 set;
              assume y in W;
              then consider x being 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 by XBOOLE_0:def 9;
      end;
      then consider m being set such that
A32:  m in H and
A33:  for C being 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 being 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 being 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,Def4;
    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 is 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 being set 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 being 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
  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 being Element of N st $1 = Ball(x,r);
  consider G being 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 being 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 being 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 being 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 being 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;

  attr N is bounded means
  :Def6:
  ex r st 0<r & for x,y being Point of N holds dist(x,y)<=r;
  let C be Subset of N;
  attr C is bounded means
  :Def7:
  ex r st 0<r & for x,y being 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 being Point of N;
A1: N = MetrStruct (#A,discrete_dist A#) & dist(x,y) = (the distance of N)
    .(x,y) by METRIC_1:def 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 Th10:
  for C being Subset of N holds ( C <> {} & C is bounded implies
ex r,w st 0<r & w in C & for z being Point of N st z in C holds dist(w,z)<=r )
& (N is symmetric triangle & (ex r,w st 0<r & for z being 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 being
  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 being Point of N st x in C & y in C holds dist(x,y)<=r by Def7;
    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 being 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 being 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 by Def7;
end;

theorem Th11:
  for r being real number holds N is Reflexive & 0<r implies w in Ball(w,r)
proof
  let r be real number;
  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 Th12:
  for r being real number holds r<=0 implies Ball(t1,r) = {}
proof
  let r be real number;
  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 being real number holds 0<r implies Ball(t1,r) is bounded
proof
  let r be real number;
  assume
A1: 0<r;
  set P = Ball(t1,r);
  reconsider r as Real by XREAL_0:def 1;
  ex r,t1 st 0<r & t1 in P & for z being 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 number;
  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 Th13:
  for P, Q being 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 being 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 being 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 being Real,t1 st 0<t & t1 in P \/ Q & for z being Point of T
        st z in P \/ Q holds dist(t1,z)<=t
        proof
          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 Th14:
  for C, D being 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 being Point of N st x in C & y in C holds dist(x,y)<=r by A1,Def7;
  ex r st 0<r & for x,y being 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 by Def7;
end;

theorem Th15:
  for P being 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 Th16:
  for P being Subset of T holds P is finite implies P is bounded
proof
  let P be Subset of T;
  defpred P[set] means ex X being Subset of T st X = $1 & X is bounded;
  {}T is bounded;
  then
A1: P[{}];
A2: for x,B being 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 being Subset of T such that
A5: X = B & X is bounded by A4;
A6: W is bounded by Th15;
    ex Y being 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 Th17:
  Y is finite & (for P being 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 being Subset of T st P in Y holds P is bounded;
  defpred P[set] means ex X being Subset of T st X = union $1 & X is bounded;
A3: for x,B being 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 being 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 being 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 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 being Point of N holds dist(x,y)<=r by Def6;
    for x,y being Point of N st x in [#]N & y in [#]N holds dist(x,y ) <=
    r by A2;
    hence thesis by A1,Def7;
  end;
  assume [#]N is bounded;
  then consider r such that
A3: 0<r and
A4: for x,y being Point of N st x in [#]N & y in [#]N holds dist(x,y)<=r
  by Def7;
  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
  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 ex x being Element of T st P = Ball(x,1) by Def1;
  for P being 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 being 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;
  func diameter C -> Real means
  :Def8:
  (for x,y being Point of N st x in C &
y in C holds dist(x,y)<=it) & for s st (for x,y being 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 being Real st (for x,y being Point of N st x in
C & y in C holds dist(x,y)<=r) & for s st for x,y being 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 being Point of N st x in C & y in C holds
      dist(x,y)<=$1;
      set I = { r : X[r] };
      defpred X[set] means ex x,y being Point of N st x in C & y in C & $1 =
      dist(x,y);
      set J = { r : X[r] };
A2:   for a,b being real number st a in J & b in I holds a<=b
      proof
        let a,b be real number;
        assume a in J & b in I;
        then
        (ex t being Real st t = a & ex x,y being Point of N st x in C & y
in C & t = dist(x,y) )& ex t9 being Real st t9=b & for x,y being 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:   0 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 being Point of N st x in C & y in C holds dist(x,y)<=r
      by A1,Def7;
A8:   r in I by A7;
      reconsider I as Subset of REAL by A6;
      consider d being real number such that
A9:   for a being real number st a in J holds a<=d and
A10:  for b being real number st b in I holds d<=b by A8,A5,A2,MEMBERED:37;
      take d;
      thus d is Real by XREAL_0:def 1;
      thus for x,y being Point of N st x in C & y in C holds dist(x,y)<=d
      proof
        let x,y be Point of N;
        assume x in C & y in C;
        then dist(x,y) in J;
        hence thesis by A9;
      end;
      let s;
      assume for x,y being Point of N st x in C & y in C holds dist(x,y)<=s;
      then s in I;
      hence thesis by A10;
    end;
    thus thesis;
  end;
  uniqueness
  proof
    let r1,r2 be Real;
    hereby
      assume C <> {};
      assume ( for x,y being Point of N st x in C & y in C holds dist(x,y)<=
r1)&( ( for s st for x,y being Point of N st x in C & y in C holds dist(x,y)<=
s holds r1<=s) & for x,y being Point of N st x in C & y in C holds dist(x,y)<=
r2 ) & for s st for x,y being 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
  for P being 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 being Point of T st x in P & y in P holds dist(x,y)<=0) & for s
st (for x,y being Point of T st x in P & y in P holds dist(x,y)<=s) holds 0<=s
  proof
    thus for x,y being 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 being 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 Th21:
  for S being 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
  for A being Subset of M holds A <> {} & A is bounded & diameter A = 0
  implies ex g being 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 being 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 being 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
  0<r implies diameter Ball(t1,r) <= 2*r
proof
A1: for x,y being 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
  for S, V being 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 being 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
  for P, Q being 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 being 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
  for S1 being 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 by Def4;
  defpred X[set] means ex n st p<=n & $1 = S1.n;
  reconsider B = {t1 where t1 is 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 is 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;
      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;
        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 : 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 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 Element of 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 : 1<=k & k<=p } by A12,FINSEQ_1:def 1;
          then ex k 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:1;
  end;
A13: A = B \/ C
  proof
    thus A c= B \/ C
    proof
      let x;
      assume x in A;
      then consider y such that
A14:  y in dom S1 and
A15:  x = S1.y by FUNCT_1:def 3;
      reconsider y as Element of 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;
    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;
      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;
      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 being 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;