:: Complete Spaces
::  by Karol P\c{a}k
:: 
:: Received October 12, 2007
:: Copyright (c) 2007 Association of Mizar Users

environ

 vocabularies WELLFND1, FRECHET2, REARRAN1, BOOLE, PRE_TOPC, COMPTS_1,
      SETFAM_1, METRIC_1, SUBSET_1, PCOMPS_1, RELAT_1, ORDINAL2, LATTICES,
      SEQ_2, PROB_1, SEQ_1, FUNCT_1, FRECHET, ARYTM_3, ARYTM, ARYTM_1,
      NORMSP_1, INT_1, ZF_REFLE, RELAT_2, ABSVALUE, FINSET_1, TARSKI, BHSP_3,
      TBSP_1, URYSOHN1, CARD_1, RLVECT_3, PARTFUN1, WELLORD1, METRIC_6,
      TOPGEN_1, RAT_1, CARD_4, AMI_1, ORDERS_1, WAYBEL23, SQUARE_1, COMPL_SP;
 notations BHSP_3, METRIC_6, RELAT_2, BINOP_1, URYSOHN1, TOPMETR, CARD_1,
      CANTOR_1, WELLORD1, COMPLEX1, FINSET_1, SEQ_2, TARSKI, XBOOLE_0,
      SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, ZFMISC_1, XXREAL_0, XREAL_0,
      REAL_1, NAT_1, SETFAM_1, DOMAIN_1, STRUCT_0, PRE_TOPC, TOPS_2, COMPTS_1,
      RELAT_1, FUNCT_1, SEQ_1, TBSP_1, RELSET_1, PARTFUN1, FUNCT_2, METRIC_1,
      PCOMPS_1, CARD_3, PROB_1, SEQM_3, FRECHET, KURATO_2, WELLFND1, WAYBEL23,
      ORDERS_2, CARD_4, TOPGEN_1, FLANG_1;
 constructors REAL_1, NAT_1, TBSP_1, YELLOW_6, FRECHET, FRECHET2, KURATO_2,
      COMPLEX1, SEQ_2, TOPS_2, WELLORD1, CARD_4, CANTOR_1, URYSOHN3, METRIC_6,
      REALSET1, WELLFND1, TOPGEN_4, WAYBEL23, TOPGEN_1, FLANG_1;
 registrations REALSET1, TOPMETR, PRE_TOPC, PCOMPS_1, NAT_1, TBSP_1, XREAL_0,
      RELSET_1, SUBSET_1, STRUCT_0, TOPS_1, METRIC_1, METRIC_3, HAUSDORF,
      MEMBERED, ORDINAL1, XXREAL_0, YELLOW13, CARD_1, WAYBEL12, ORDERS_2,
      XBOOLE_0;
 requirements REAL, SUBSET, BOOLE, NUMERALS, ARITHM;
 definitions TARSKI, TOPS_2, SUBSET_1, STRUCT_0, TBSP_1, PCOMPS_1, COMPTS_1,
      METRIC_1;
 theorems KURATO_2, NAT_1, FUNCT_2, PCOMPS_1, PCOMPS_2, NAGATA_1, SUBSET_1,
      METRIC_6, FUNCT_1, METRIC_1, XREAL_0, XCMPLX_1, ABSVALUE, TOPMETR,
      XBOOLE_1, TARSKI, SETFAM_1, XBOOLE_0, TOPS_1, TOPS_2, PRE_TOPC, FINSET_1,
      CARD_4, ZFMISC_1, BINOP_1, SEQ_2, SEQ_4, SEQ_1, SEQM_3, PARTFUN1,
      WELLORD1, WELLORD2, TBSP_1, RELAT_1, RELAT_2, YELLOW_9, XREAL_1,
      XXREAL_0, ORDINAL1, RELSET_1, FRECHET2, FRECHET, COMPTS_1, STIRL2_1,
      CARD_1, EULER_1, HAUSDORF, TOPMETR3, CARD_3, TOPGEN_4, STRUCT_0, DICKSON,
      RELSET_2, TOPGEN_1, YELLOW13, WELLFND1, CARD_FIL, WAYBEL23, UNIFORM1,
      CARD_2;
 schemes FUNCT_1, WELLFND1, TREES_2, FUNCT_2, NAT_1, FRAENKEL, BINOP_1,
      KURATO_2, SEQ_1;

begin :: Preliminaries

reserve i,j,n,m for natural number,
        x,y,X,Y for set,
        r,s for Real;

definition 
  let M be non empty MetrStruct;
  let S be SetSequence of M; 
  attr S is bounded means :def1:
    for i holds S.i is bounded;
end;

registration
  let M be non empty Reflexive MetrStruct;
  cluster bounded non-empty SetSequence of M; 
  existence
    proof
      consider x such that
A1:     x in the carrier of M by XBOOLE_0:def 1;
      reconsider x as Point of M by A1;
      reconsider X={x} as Subset of M;
A2:   now let x1,x2 being Point of M such that A3:x1 in X & x2 in X;
         x1=x & x2=x by A3,TARSKI:def 1;
         hence dist(x1,x2)<=1 by METRIC_1:1;
      end;
      deffunc F(set)=X;
      consider S being SetSequence of M such that
A3:     for n being Element of NAT holds S.n = F(n) from KURATO_2:sch 1;    
      take S;
A4:   now let i; 
         reconsider i'=i as Element of NAT by ORDINAL1:def 13;
         X is bounded & S.i'=F(i) by A2,A3,TBSP_1:def 9;
         hence S.i is bounded;
      end;
      for x st x in dom S holds S.x is non empty by A3;
      hence thesis by A4,def1,FUNCT_1:def 15;
    end;
end;

definition let M be Reflexive non empty MetrStruct;
  let S be SetSequence of M; 
  func diameter S -> Real_Sequence means :def2:
    for i holds it.i = diameter S.i;
  existence
    proof   
      defpred P[set,set] means for i st i=$1 holds $2=diameter (S.i);
A1:   for x st x in NAT ex y st y in REAL & P[x,y]
        proof
          let x such that A2:x in NAT;
          reconsider i=x as Element of NAT by A2;
          take diameter (S.i);
          thus thesis by XREAL_0:def 1;
        end;
      consider f be Function of NAT,REAL such that 
A2:     for x st x in NAT holds P[x,f.x] from FUNCT_2:sch 1(A1);
      take f;
      let i;
      i in NAT by ORDINAL1:def 13;        
      hence thesis by A2;
    end;
  uniqueness
    proof
      let D1,D2 be Real_Sequence such that
A1:     for i holds D1.i = diameter S.i and
A2:     for i holds D2.i = diameter S.i;
      now let x such that A3:x in NAT;
         reconsider i=x as Element of NAT by A3;
         thus D1.x = diameter S.i by A1
                  .= D2.x by A2;
      end;
      hence thesis by SEQ_1:8;
    end;
end;

theorem Th1:
  for M be Reflexive non empty MetrStruct
    for S be bounded SetSequence of M holds
      diameter S is bounded_below
proof
  let M be Reflexive non empty MetrStruct;
  let S be bounded SetSequence of M;set d=diameter S;
  now let n be Element of NAT;    
     S.n is bounded & diameter (S.n)=d.n by def1,def2;
     then 0<=d.n by TBSP_1:29;
     hence -1 < d.n by XXREAL_0:2;
  end;
  hence thesis by SEQ_2:def 4;  
end;

theorem Th2:
  for M be Reflexive non empty MetrStruct
    for S be bounded SetSequence of M st S is descending holds
      diameter S is bounded_above & diameter S is non-increasing
proof
  let M be Reflexive non empty MetrStruct;
  let S be bounded SetSequence of M such that 
A1:S is descending;
  set d=diameter S;
A2:now let n be Element of NAT; 
     S.n c= S.0 & S.0 is bounded & diameter S.n=d.n & diameter S.0=d.0
       by A1,KURATO_2:22,def1,def2;
     then d.n<=d.0 & d.0+0<d.0+1 by TBSP_1:32,XREAL_1:10;
     hence d.n<d.0+1 by XXREAL_0:2;
  end;
  now let m,n be Element of NAT such that 
  A3:m in dom d & n in dom d & m <= n;
     S.n c= S.m & S.m is bounded & diameter S.n=d.n & diameter S.m=d.m
        by def1,def2,A1,A3,KURATO_2:22;
     hence d.n<=d.m  by TBSP_1:32;
  end;
  hence thesis by A2,SEQ_2:def 3,SEQM_3:def 4;
end;

theorem
  for M be Reflexive non empty MetrStruct
    for S be bounded SetSequence of M st S is ascending holds
      diameter S is non-decreasing
proof
  let M be Reflexive non empty MetrStruct;
  let S be bounded SetSequence of M such that 
A1: S is ascending;
  set d=diameter S;
  now let m,n be Element of NAT such that 
  A2: m in dom d & n in dom d & m <= n; 
     S.m c= S.n & S.n is bounded & diameter S.n=d.n & diameter S.m=d.m
       by def1,def2,A1,A2,KURATO_2:23;
     hence d.n>=d.m  by TBSP_1:32;
  end;
  hence thesis by SEQM_3:def 3;
end;

theorem Th4:
  for M be non empty Reflexive MetrStruct
    for S be bounded SetSequence of M st 
        S is descending & lim diameter S = 0 
        for F be sequence of M st for i holds F.i in S.i 
      holds F is Cauchy
proof
  let M be non empty Reflexive MetrStruct;
  let S be bounded SetSequence of M such that 
A1: S is descending & lim diameter S = 0;set d=diameter S;
  let F be sequence of M such that 
A2: for i holds F.i in S.i;
  let r such that 
A3: r>0;
  d is bounded_below & d is non-increasing by A1,Th1,Th2;
  then d is convergent by SEQ_4:52;
  then consider n be Element of NAT such that
A4: for m be Element of NAT st n <= m holds abs(d.m-0) < r 
    by A1,A3,SEQ_2:def 7;
  take n;
  let m1,m2 be Element of NAT such that 
A5:n <= m1 & n <= m2;
  S.m1 c= S.n & S.m2 c= S.n & F.m1 in S.m1 & F.m2 in S.m2 
    by A1,A2,A5,KURATO_2:22;
  then F.m1 in S.n & F.m2 in S.n & S.n is bounded & diameter S.n=d.n
    by def1,def2;
  then A5:dist(F.m1,F.m2)<=d.n & 0 <= d.n & abs(d.n-0)<r 
    by A4,TBSP_1:def 10,29;
  then d.n < r by ABSVALUE:def 1; 
  hence thesis by A5,XXREAL_0:2;
end;

Th5: :: generalized TOPREAL6:67
  for r being real number
    for M be Reflexive symmetric triangle non empty MetrStruct
      for x be Element of M holds cl_Ball(x,r) is bounded
proof
  let r being real number;
  let M be Reflexive symmetric triangle non empty MetrStruct;
  let x be Element of M;
A1:cl_Ball(x,r) c= Ball(x,r+1)
    proof
      let y such that 
  A2:   y in cl_Ball(x,r);
      reconsider Y=y as Point of M by A2;
      dist(x,Y)<=r & r+0<r+1 by A2,METRIC_1:13,XREAL_1:10;
      then dist(x,Y)<r+1 by XXREAL_0:2;
      hence thesis by METRIC_1:12;
    end;
  Ball(x,r+1) is bounded by TBSP_1:19;
  hence thesis by A1,TBSP_1:21;
end;

theorem Th6:
  for M be Reflexive symmetric triangle non empty MetrStruct 
    for p be Point of M holds
      0 <= r implies diameter cl_Ball(p,r) <= 2*r
proof
  let M be Reflexive symmetric triangle non empty MetrStruct;
  let p be Point of M;assume 
A1:0 <= r;
A2:cl_Ball(p,r) is bounded by Th5;
  dist(p,p)=0 by METRIC_1:1;then
A3:p in cl_Ball(p,r) by A1,METRIC_1:13;
  now let x,y be Point of M such that 
  A4: x in cl_Ball(p,r) & y in cl_Ball(p,r);
     dist(p,y)<=r & dist(x,p)<=r by A4,METRIC_1:13;
     then dist(x,y)<=dist(x,p)+dist(p,y) & dist(x,p)+dist(p,y)<=r+r 
       by XREAL_1:9,METRIC_1:4;
     hence dist(x,y)<=2*r by XXREAL_0:2;
  end;
  hence thesis by A2,A3,TBSP_1:def 10;
end;

definition
  let M be MetrStruct;
  let U be Subset of M;
  attr U is open means :def3:
    U in Family_open_set M;
end;

definition
  let M be MetrStruct;
  let A be Subset of M;
  attr A is closed means :def4:
    A` is open;
end;

registration
  let M be MetrStruct;
  cluster open empty Subset of M;
  existence
    proof  
      TopSpaceMetr(M) = TopStruct (#the carrier of M,Family_open_set M#);
      then {} in Family_open_set M by PRE_TOPC:5;
      then {}M is open by def3;
      hence thesis;
    end;
  cluster closed empty Subset of M;
  existence
    proof
      [#]M in Family_open_set M by PCOMPS_1:34;
      then [#]M is open & [#]M=([#]M)`` & [#]M = ({}M)` by def3;
      then ([#]M)` is closed & ([#]M)`={}M by def4;
      hence thesis;
    end;
end;

registration
  let M be non empty MetrStruct;
  cluster open non empty Subset of M;
  existence
    proof
      [#]M in Family_open_set M by PCOMPS_1:34;
      then [#]M is open by def3;
      hence thesis;
    end;
  cluster closed non empty Subset of M;
  existence
    proof
      consider A be open empty Subset of M;
      A``=A;
      then A`=[#]M & A` is closed by def4;
      hence thesis;
    end;
end;

theorem Th7:
  for M be MetrStruct
    for A be Subset of M, A' be Subset of TopSpaceMetr M st A' = A 
      holds 
  ( A is open iff A' is open ) & ( A is closed iff A' is closed )
proof
  let M be MetrStruct;
  set T=TopSpaceMetr(M);
  let A be Subset of M, A' be Subset of TopSpaceMetr M such that 
A1: A' = A;
  thus A is open implies A' is open 
    proof
      assume A is open;
      then A in Family_open_set M by def3;
      hence thesis by A1,PRE_TOPC:def 5;
    end;
  thus A' is open implies A is open 
    proof
      assume A' is open;
      then A' in Family_open_set M by PRE_TOPC:def 5;
      hence thesis by A1,def3;
    end;
  thus A is closed implies A' is closed
    proof
      assume A is closed;
      then A` is open by def4;
      then A` in Family_open_set M by def3;
      then A'` is open by A1,PRE_TOPC:def 5;
      hence thesis by TOPS_1:29;
    end;
  assume A' is closed;
  then A'` is open by TOPS_1:29;
  then A` in Family_open_set M by A1,PRE_TOPC:def 5;
  then A` is open by def3;
  hence thesis by def4;
end;

definition
  let T be TopStruct;
  let S be SetSequence of T; 
  attr S is open means :def5:
    for i holds S.i is open;
  attr S is closed means :def6:
    for i holds S.i is closed;
end;

LM:for T be TopSpace ex S be SetSequence of T st 
  S is open & S is closed & (T is non empty implies S is non-empty)
proof
  let T be TopSpace;
  deffunc F(set)=[#]T;
  consider S being SetSequence of T such that
A1: for n being Element of NAT holds S.n = F(n) from KURATO_2:sch 1;    
  take S;
A2:now let i;
     i in NAT by ORDINAL1:def 13;
     hence S.i is open by A1;
  end;
  now let i;
     i in NAT by ORDINAL1:def 13;
     hence S.i is closed by A1;
  end;
  hence S is open & S is closed by A2,def5,def6;
  assume 
A3:T is non empty;
  now let x such that 
  A4:x in dom S;
     S.x=[#]T & [#]T is non empty by A1,A3,A4,STRUCT_0:def 1;
     hence S.x is non empty;
  end;
  hence thesis by FUNCT_1:def 15;
end;

registration
  let T be TopSpace;
  cluster open SetSequence of T;
  existence 
    proof
      ex S be SetSequence of T st S is open & S is closed &
         (T is non empty implies S is non-empty) by LM;
      hence thesis;
    end;
  cluster closed SetSequence of T;
  existence
    proof
      ex S be SetSequence of T st S is open & S is closed &
         (T is non empty implies S is non-empty) by LM;
      hence thesis;
    end;
end;

registration
  let T be non empty TopSpace;
  cluster open non-empty SetSequence of T;
  existence
    proof
      ex S be SetSequence of T st S is open & S is closed &
         (T is non empty implies S is non-empty) by LM;
      hence thesis;
    end;
  cluster closed non-empty SetSequence of T;
  existence
    proof
      ex S be SetSequence of T st S is open & S is closed &
         (T is non empty implies S is non-empty) by LM;
      hence thesis;
    end;
 end;

definition
  let M be MetrStruct;
  let S be SetSequence of M; 
  attr S is open means :def7:
    for i holds S.i is open;
  attr S is closed means :def8:
    for i holds S.i is closed;
end;

registration
  let M be non empty MetrSpace;
  cluster non-empty bounded open SetSequence of M; 
  existence
    proof
      consider x such that
  A1:   x in the carrier of M by XBOOLE_0:def 1;
      reconsider x as Point of M by A1;
      set B=Ball(x,1);
      deffunc F(set)=B;
      consider S being SetSequence of M such that
  A2:   for n being Element of NAT holds S.n = F(n) from KURATO_2:sch 1;    
      take S;
  A3: now let i;
         B is bounded & i in NAT by TBSP_1:19,ORDINAL1:def 13;
         hence S.i is bounded by A2;
      end;
  A4: now let y such that 
      A5: y in dom S;
         reconsider n=y as Element of NAT by A5;
         dist(x,x)=0 by METRIC_1:1;
         then x in B & B=S.n by A2,METRIC_1:12;
         hence S.y is non empty;
      end;
      now let i;
         i in NAT by ORDINAL1:def 13;
         then S.i=B & B in Family_open_set(M) by A2,PCOMPS_1:33;
         hence S.i is open by def3;
      end;
      hence thesis by A3,A4,def1,def7,FUNCT_1:def 15;    
    end;
  cluster non-empty bounded closed SetSequence of M; 
  existence
    proof
      consider x such that
  A1:   x in the carrier of M by XBOOLE_0:def 1;
      reconsider x as Point of M by A1;
      set B=cl_Ball(x,1);
      deffunc F(set)=B;
      consider S being SetSequence of M such that
   A3:  for n being Element of NAT holds S.n = F(n) from KURATO_2:sch 1;    
    take S;
    A4:now let i; 
        B is bounded & i in NAT by Th5,ORDINAL1:def 13;
        hence S.i is bounded by A3;
    end;
    A5:now let y such that A6:y in dom S;
      reconsider n=y as Element of NAT by A6;      
      dist(x,x)=0 by METRIC_1:1;
      then x in B & B=S.n by A3,METRIC_1:13;
      hence S.y is non empty;
    end;
    now let i;
       i in NAT & [#]M\B in Family_open_set(M) 
        by NAGATA_1:14,ORDINAL1:def 13;
      then B` is open & S.i=B by A3,def3;
      hence S.i is closed by def4;
    end;
    hence thesis by A4,A5,def1,def8,FUNCT_1:def 15;    
  end;
end;

theorem Th8:
  for M be MetrStruct
    for S be SetSequence of M, S' be SetSequence of TopSpaceMetr M st S' = S 
      holds 
  ( S is open iff S' is open ) & ( S is closed iff S' is closed )
proof
  let M be MetrStruct;
  let S be SetSequence of M, S' be SetSequence of TopSpaceMetr M such that 
    A1:S' = S;
  thus S is open implies S' is open 
  proof
    assume A2:S is open;
    let i;
    S.i is open by A2,def7;
    hence thesis by A1,Th7;
  end;
  thus S' is open implies S is open 
  proof
    assume A2:S' is open;
    let i;
    S'.i is open by A2,def5;
    hence thesis by A1,Th7;
  end;
  thus S is closed implies S' is closed 
  proof
    assume A2:S is closed;
    let i;
    S.i is closed by A2,def8;
    hence thesis by A1,Th7;
  end;
assume A2:S' is closed;
    let i;
    S'.i is closed by A2,def6;
    hence thesis by A1,Th7;
end;
 
theorem Th9:
  for M be Reflexive symmetric triangle non empty MetrStruct
    for S, CL be Subset of M st S is bounded
      for S' be Subset of TopSpaceMetr M st S = S' & CL = Cl S'
        holds CL is bounded & diameter S = diameter CL
proof
  let M be Reflexive symmetric triangle non empty MetrStruct;
  let S,CL be Subset of M such that 
A1: S is bounded;
  set T=TopSpaceMetr M;set d=diameter S;
  let S' be Subset of T such that 
A2: S = S' & CL = Cl S';
  per cases;
    suppose A3:S<>{};then 
  A4: CL<>{} by A2,PCOMPS_1:2;
      d >= 0 by A1,TBSP_1:29;then
  A5: d+1>0+0 by XREAL_1:10;
  A6: now let x,y be Point of M such that 
      A7: x in CL & y in CL; assume
      A8:dist(x,y) > d;
         set dxy=dist(x,y);set dd=dxy-d;set dd2=dd/2;
         set Bx=Ball(x,dd2);set By=Ball(y,dd2);  
         reconsider BX=Bx,BY=By as Subset of T;
         reconsider X=x,Y=y as Point of T;
         dd > d-d by A8,XREAL_1:16;then
      A9:dd2>0/2 by XREAL_1:76;
         dist(x,x)=0 & dist(y,y)=0 & Bx in Family_open_set M & 
           By in Family_open_set M by METRIC_1:1,PCOMPS_1:33;
         then X in BX & Y in BY & BX is open & BY is open
           by A9,METRIC_1:12,PRE_TOPC:def 5;then
      A10:BX meets S' & BY meets S' by A2,A7,TOPS_1:39;
         then consider x1 be set such that
      A11:x1 in BX & x1 in S' by XBOOLE_0:3;
         consider y1 be set such that
      A12:y1 in BY & y1 in S' by A10,XBOOLE_0:3;
         reconsider x1,y1 as Point of M by A11,A12;
      A13:dist(x1,y1)<=d & dist(x,x1)<dd2 & dist(y,y1)<dd2 
           by A1,A2,A11,A12,TBSP_1:def 10,METRIC_1:12;
         then dist(x,y1)<=dist(x,x1)+dist(x1,y1) & dist(x,x1)+dist(x1,y1)<dd2+d
           & dist(y1,y) < dd2 by XREAL_1:10,METRIC_1:4;
         then dist(x,y1)<dd2+d by XXREAL_0:2;
         then dist(x,y)<=dist(x,y1)+dist(y1,y)&dist(x,y1)+dist(y1,y)< dd2+d+dd2
           by A13,XREAL_1:10,METRIC_1:4;
         hence contradiction;
      end;
      now let x,y be Point of M such that 
      A7: x in CL & y in CL;
         dist(x,y)<=d & d+0<d+1 by A6,A7,XREAL_1:10;
         hence dist(x,y) <= d+1 by XXREAL_0:2;
      end;then
  A7: CL is bounded by A5,TBSP_1:def 9;
      now let s such that 
      A8: for x,y be Point of M st x in CL & y in CL holds dist(x,y)<=s;
         now let x,y be Point of M such that 
         A9: x in S & y in S; 
            S c= CL by A2,PRE_TOPC:48;          
            hence dist(x,y)<=s by A8,A9;
         end;
         hence d <= s by A1,A3,TBSP_1:def 10;
      end;
      hence thesis by A4,A6,A7,TBSP_1:def 10;end;
    suppose S={};
       hence thesis by A1,A2,PCOMPS_1:2;end;
end;

begin :: Cantor's theorem on complete spaces

theorem Th10:
  for M be non empty MetrSpace
    for C be sequence of M
      ex S be non-empty closed SetSequence of M st
          S is descending & 
        ( C is Cauchy implies S is bounded & lim diameter S = 0 ) &
          for i ex U be Subset of TopSpaceMetr M st 
            U = { C.j where j is Element of NAT: j >= i } & S.i = Cl U
proof
  let M be Reflexive symmetric triangle non empty MetrSpace;
  set T=TopSpaceMetr(M);
  let C be sequence of M;
  defpred P[set,set] means for i st i=$1 ex S be Subset of T st 
      S={C.j where j is Element of NAT: j >= i} & $2=Cl S;
A1:for x st x in NAT ex y st y in bool(the carrier of M) & P[x,y]
    proof
      let x such that 
    A2: x in NAT;
      reconsider x'=x as Element of NAT by A2;
      set S={C.j where j is Element of NAT: j >= x'};
      S c= the carrier of T
        proof
          let y such that A3:y in S;
          ex j be Element of NAT st C.j=y & j>=x' by A3;
          hence thesis;
        end;
      then reconsider S as Subset of T;
      take CL=Cl S;
      thus thesis;
    end;
  consider S be SetSequence of M such that
A2: for x st x in NAT holds P[x,S.x] from FUNCT_2:sch 1(A1);
A3:now let x such that 
  A4: x in dom S;
     reconsider i=x as Element of NAT by A4;
     consider U be Subset of T such that
  A5:  U={C.j where j is Element of NAT: j >= i} & S.i=Cl U by A2;
     C.i in U & U c= S.i by A5,PRE_TOPC:48;
     hence S.x is non empty;
  end;
A4:now let i; 
     i in NAT by ORDINAL1:def 13;
     then ex U be Subset of T st
       U={C.j where j is Element of NAT: j >= i} & S.i=Cl U by A2;
     hence S.i is closed by Th7;
  end;
  reconsider S as non-empty closed SetSequence of M
    by A3,A4,def8,FUNCT_1:def 15;
  take S;
  now let i be Element of NAT;
     consider U be Subset of T such that
  A6:  U={C.j where j is Element of NAT: j >= i} & S.i=Cl U by A2;
     consider U1 be Subset of T such that
  A7:  U1={C.j where j is Element of NAT: j >= i+1} & S.(i+1)=Cl U1 by A2;
     U1 c= U
       proof
         let x such that 
     A8:   x in U1;
         consider j be Element of NAT such that 
     A9:   x=C.j & j>=i+1 by A7,A8;
         j>= i by A9,NAT_1:13;
         hence thesis by A6,A9; 
       end;
     hence S.(i+1) c= S.i by A6,A7,PRE_TOPC:49;
  end;
  hence A5':S is descending by KURATO_2:def 5;
  thus C is Cauchy implies S is bounded & lim diameter S = 0
    proof
      assume 
  A6:   C is Cauchy;
  A7: now let i;
         i in NAT by ORDINAL1:def 13;
         then consider U be Subset of T such that
     A8:   U={C.j where j is Element of NAT: j >= i} & S.i=Cl U by A2;
         reconsider U'=U as Subset of M;
     A9:   U c= rng C
           proof
             let x such that 
         A10:  x in U;
             dom C=NAT & ex j be Element of NAT st x=C.j & j>=i 
               by A8,A10,FUNCT_2:def 1;
             hence thesis by FUNCT_1:def 5;
           end;
         rng C is bounded by A6,TBSP_1:34;
         then U' is bounded by A9,TBSP_1:21;
         hence S.i is bounded by A8,Th9;
      end;
      hence S is bounded by def1;
      reconsider S'=S as non-empty bounded closed SetSequence of M 
        by A7,def1;
      set d=diameter S';
      d is bounded_below & d is non-increasing by A5',Th1,Th2;then 
  A8: d is convergent by SEQ_4:52;
      for r be real number st 0<r ex n be Element of NAT st 
        for m be Element of NAT st n<=m holds abs(d.m-0)<r
        proof
          let r be real number such that 
        A9: 0<r;
          reconsider R=r as Real by XREAL_0:def 1;
          set R2=R/2;
          R2>0 by A9,XREAL_1:141;
          then consider p be Element of NAT such that
       A10: for n,m be Element of NAT st p<=n & p<=m holds 
          dist(C.n,C.m)<R2 by A6,TBSP_1:def 5;
          take p;
          let m be Element of NAT such that 
       A11: p<=m;
          consider U be Subset of T such that
       A12: U={C.j where j is Element of NAT: j >= m} & S.m=Cl U by A2;
          reconsider CL=Cl U,U'=U as Subset of M;
       A13: U c= rng C
             proof
               let x such that 
             A14: x in U;
               dom C=NAT & ex j be Element of NAT st x=C.j & j>=m 
                 by A12,A14,FUNCT_2:def 1;
               hence thesis by FUNCT_1:def 5;
             end;
          rng C is bounded & C.m in U by A6,A12,TBSP_1:34;then
       A14:U' is bounded & U' is non empty by A13,TBSP_1:21;
          now let x,y being Point of M such that 
          A15: x in U' & y in U';
              consider i be Element of NAT such that
          A16: x = C.i & i>=m by A12,A15;
              consider j be Element of NAT such that
          A17: y=C.j & j>=m by A12,A15;
              i>=p & j>=p by A11,A16,A17,XXREAL_0:2;
              hence dist(x,y)<=R2 by A10,A16,A17;
          end;
          then diameter U'<=R2 & diameter U'=diameter S.m 
            by A12,A14,TBSP_1:def 10,Th9;
          then diameter S.m <= R2 & diameter S.m>=0 by A14,TBSP_1:29;
          then abs(diameter S.m)<=R2 & R2<R by A9,XREAL_1:218,ABSVALUE:def 1;
          then abs(diameter S.m)<R & diameter S.m=d.m by def2,XXREAL_0:2;
          hence thesis;
        end;
      hence lim diameter S = 0 by A8,SEQ_2:def 7;
    end;
  let i;
  i in NAT by ORDINAL1:def 13;
  hence thesis by A2;
end;

theorem Th11:
  for M be non empty MetrSpace holds
    M is complete iff
           for S be non-empty bounded closed SetSequence of M st
             S is descending & lim diameter S = 0 holds meet S is non empty
proof
  let M be non empty MetrSpace;
  set T=TopSpaceMetr(M);
  thus M is complete implies
     for S be non-empty bounded closed SetSequence of M st
        S is descending & lim diameter S = 0 holds meet S is non empty
    proof assume 
  A1: M is complete;
      let S be non-empty bounded closed SetSequence of M such that
  A2:   S is descending & lim diameter S = 0;
      defpred P[set,set] means $2 in S.$1;
  A3: for x st x in NAT ex y st y in the carrier of M & P[x,y]
        proof
          let x such that 
      A4:  x in NAT;
      A5: dom S=NAT by FUNCT_2:def 1;    
          then S.x is non empty by A4,FUNCT_1:def 15;
          then consider y such that 
      A6:   y in S.x by XBOOLE_0:def 1;
          S.x in rng S& rng S c= bool (the carrier of M)by A4,A5,FUNCT_1:def 5;
          hence thesis by A6;
        end;
      consider F be Function of NAT,the carrier of M such that
  A4:   for x st x in NAT holds P[x,F.x] from FUNCT_2:sch 1(A3);
      now let i;
         i in NAT by ORDINAL1:def 13;
         hence F.i in S.i by A4;
      end;
      then F is Cauchy by A2,Th4;
      then F is convergent by A1,TBSP_1:def 6;
      then consider x be Point of M such that       
  A5:   F is_convergent_in_metrspace_to x by METRIC_6:22;
      reconsider x' = x as Point of T;
      reconsider F' = F as sequence of T;
      now let i be Element of NAT;
         consider F1 be subsequence of F' such that
      A6:  for n be Element of NAT holds F1.n=F'.(n+i) by FRECHET2:42;
         reconsider Si=S.i as Subset of T;
         S.i is closed by def8;then   
      A7:Si is closed by Th7;
         rng F1 c= Si
           proof
             let x such that 
           A8: x in rng F1;
             consider y such that
           A9: y in dom F1 & F1.y=x by A8,FUNCT_1:def 5;
             reconsider y as Element of NAT by A9;
             x=F.(y+i) & i<=y+i by A6,A9,NAT_1:11;
             then x in S.(y+i) & S.(y+i) c= S.i by A2,A4,KURATO_2:22;
             hence thesis;
           end;then
      A8:Lim F1 c= Si by A7,FRECHET2:12;
         F' is_convergent_to x' by A5,FRECHET2:31;
         then F1 is_convergent_to x' by FRECHET2:18;
         then x in Lim F1 by FRECHET:def 4;
         hence x in S.i by A8;
      end;
      hence thesis by KURATO_2:6;
    end;
  assume 
A1:for S be non-empty bounded closed SetSequence of M st
     S is descending & lim diameter S = 0 holds meet S is non empty;
  let F be sequence of M such that 
A2: F is Cauchy;
  consider S be non-empty closed SetSequence of M such that
A3: S is descending and     
A4: F is Cauchy implies S is bounded & lim diameter S = 0 and
A5: for i ex U be Subset of T st 
      U={ F.j where j is Element of NAT:j >= i} & S.i = Cl U by Th10;       
  meet S is non empty by A1,A2,A3,A4;
  then consider x such that
A6: x in meet S by XBOOLE_0:def 1;
  reconsider x as Point of M by A6;
  take x;
  let r such that 
A7: r>0;
  set d=diameter S;
  d is bounded_below & d is non-increasing by A2,A3,A4,Th1,Th2;
  then d is convergent by SEQ_4:52;
  then consider n be Element of NAT such that 
A8: for m be Element of NAT st n<=m holds abs(d.m-0)<r by A2,A4,A7,SEQ_2:def 7;
  take n;
  let m be Element of NAT such that 
A9: n<=m;
  consider U be Subset of T such that
A10:U = { F.j where j is Element of NAT: j >= m } & S.m = Cl U by A5;
  F.m in U & U c= Cl U by A10,PRE_TOPC:48;
  then x in S.m & F.m in S.m & S.m is bounded by A2,A4,A6,A10,KURATO_2:6,def1;
  then dist(F.m,x) <= diameter (S.m) & diameter (S.m)>=0 & diameter (S.m)=d.m
    & abs(d.m-0)<r by A8,A9,TBSP_1:def 10,TBSP_1:29,def2;
  then dist(F.m,x) <= d.m & d.m <r by ABSVALUE:def 1;
  hence thesis by XXREAL_0:2;
end;

theorem Th12:
  for T be non empty TopSpace
    for S be non-empty SetSequence of T st S is descending
      for F be Subset-Family of T st F = rng S 
    holds F is centered
proof
  let T be non empty TopSpace;
  let S be non-empty SetSequence of T such that 
A1: S is descending;
  let F be Subset-Family of T such that 
A2: F = rng S;
  dom S=NAT by FUNCT_2:def 1; then
A3: F<>{} by A2,RELAT_1:65;
  now let G be set such that 
  A4: G <> {} & G c= F & G is finite;
     defpred P[set,set] means $1=S.$2;
  A5:for x st x in G ex y st y in NAT & P[x,y]
       proof
         let x such that 
       A6: x in G;
         ex y st y in dom S & S.y=x by A2,A4,A6,FUNCT_1:def 5;
         hence thesis;     
       end;
     consider f be Function of G,NAT such that 
  A6:  for x st x in G holds P[x,f.x] from FUNCT_2:sch 1(A5);
  A7:dom f=G by FUNCT_2:def 1;
     then rng f is finite by A4,FINSET_1:26;
     then consider i be Element of NAT such that 
  A8:  for j be Element of NAT st j in rng f holds j<=i by STIRL2_1:66;
     dom S=NAT by FUNCT_2:def 1;
     then S.i<>{} by FUNCT_1:def 15;
     then consider x such that
  A9:  x in S.i by XBOOLE_0:def 1;
     now let Y be set;
        assume 
     A10: Y in G;then
     A11:f.Y in rng f by A7,FUNCT_1:def 5; 
        then reconsider fY=f.Y as Element of NAT;
        Y=S.fY & fY <= i by A6,A8,A10,A11;
        then S.i c= Y by A1,KURATO_2:22;
        hence x in Y by A9;
     end;
     hence meet G<>{} by A4,SETFAM_1:def 1;
  end;
  hence thesis by A3,COMPTS_1:def 2;
end;

theorem Th13:
  for M be non empty MetrStruct
    for S be SetSequence of M
      for F be Subset-Family of TopSpaceMetr M st F = rng S 
    holds 
      ( S is open implies F is open ) & ( S is closed implies F is closed )
proof
  let M be non empty MetrStruct;
  let S be SetSequence of M;
  set T=TopSpaceMetr(M);
  let F be Subset-Family of T such that 
A1: F = rng S;
  thus S is open implies F is open
    proof
      assume 
  A2:   S is open;
      let P be Subset of T;
      assume P in F;
      then consider x such that
  A3:   x in dom S & S.x=P by A1,FUNCT_1:def 5;
      reconsider x as natural number by A3,ORDINAL1:def 13;
      S.x is open by A2,def7;
      hence thesis by A3,Th7;
    end;
  assume 
A2: S is closed;
  let P be Subset of T;
  assume P in F;
  then consider x such that
A3: x in dom S & S.x=P by A1,FUNCT_1:def 5;
  reconsider x as natural number by A3,ORDINAL1:def 13;
  S.x is closed by A2,def8;
  hence thesis by A3,Th7;
end;

theorem Th14:
  for T be non empty TopSpace
    for F be Subset-Family of T 
      for S be SetSequence of T st rng S c= F 
      ex R be SetSequence of T st 
        R is descending & 
       ( F is centered implies R is non-empty ) &
       ( F is open implies R is open ) & ( F is closed implies R is closed ) &
        for i holds R.i = meet {S.j where j is Element of NAT: j <= i}
proof
  let T be non empty TopSpace;
  let F be Subset-Family of T;
  let S be SetSequence of T such that 
A1: rng S c= F;
A2:for i holds {S.j where j is Element of NAT: j <= i} c= F 
    proof
      let i;
      let x such that 
  A3:   x in {S.j where j is Element of NAT : j <= i}; 
      consider j be Element of NAT such that 
  A4:   x=S.j & j<=i by A3;
      dom S=NAT by FUNCT_2:def 1;
      then x in rng S by A4,FUNCT_1:def 5;
      hence thesis by A1;
    end;
  defpred P[set,set] means
    for i st i=$1 holds $2=meet {S.j where j is Element of NAT:j<=i};
A3:for x st x in NAT ex y st y in bool(the carrier of T) & P[x,y]
    proof
      let x such that 
    A4: x in NAT;
      reconsider i=x as Element of NAT by A4;
      set SS={S.j where j is Element of NAT:j<=i};
      SS c= F by A2;
      then reconsider SS as Subset-Family of T by XBOOLE_1:1;
      take meet SS;
      thus thesis;
    end;
  consider R be SetSequence of T such that
A4: for x st x in NAT holds P[x,R.x] from FUNCT_2:sch 1(A3);
A5:for i holds {S.j where j is Element of NAT:j<=i} is finite
    proof
      let i;
      set SS={S.j where j is Element of NAT:j<=i};
      reconsider i'=i as Element of NAT by ORDINAL1:def 13;
   A6:i+1 is finite;
      deffunc F(set)=S.$1;
   A7:{F(j)where j is Element of NAT:j in i+1} is finite 
        from FRAENKEL:sch 21(A6);
      SS c= {F(j)where j is Element of NAT:j in i+1}
        proof
          let x such that 
        A8: x in SS;
          consider j be Element of NAT such that
        A9: x=S.j & j<=i by A8;
          j<i+1 by A9,NAT_1:13;
          then j in i+1 by EULER_1:1;
          hence thesis by A9;
        end;
      hence thesis by A7,FINSET_1:13;
    end;
  take R;
  now let i be Element of NAT;
     set SS={S.j where j is Element of NAT:j<=i};
     set S1={S.j where j is Element of NAT:j<=i+1};
  A6:S.0 in SS;
     SS c= S1
       proof
         let x such that 
       A7: x in SS;
         consider j be Element of NAT such that
       A8: x=S.j & j<=i by A7;
         j<=i+1 by A8,NAT_1:13;
         hence thesis by A8;
       end;
     then meet S1 c= meet SS & meet SS=R.i by A4,A6,SETFAM_1:7;
     hence R.(i+1) c= R.i by A4;
  end;
  hence R is descending by KURATO_2:def 5;
  thus F is centered implies R is non-empty
    proof
      assume 
    A6:F is centered;
      now let x such that 
      A7: x in dom R;
         reconsider i=x as Element of NAT by A7;
         set SS={S.j where j is Element of NAT:j<=i};
         SS is finite & S.0 in SS & SS c= F by A2,A5;
         then meet SS<>{} by A6,COMPTS_1:def 2;
         hence R.x is non empty by A4;
      end;
      hence thesis by FUNCT_1:def 15;
    end;
  thus F is open implies R is open
    proof
      assume 
    A6: F is open;
      let i;
      set SS={S.j where j is Element of NAT:j<=i};
    A7:SS c= F by A2;
      then reconsider SS as Subset-Family of T by XBOOLE_1:1;
      SS is open & SS is finite & i in NAT 
        by A5,A6,A7,TOPS_2:18,ORDINAL1:def 13;
      then meet SS is open & R.i=meet SS by A4,TOPS_2:27;
      hence thesis;
    end;
  thus F is closed implies R is closed
    proof
      assume 
    A6: F is closed;
      let i;
      set SS={S.j where j is Element of NAT:j<=i};
    A7:SS c= F by A2;
      then reconsider SS as Subset-Family of T by XBOOLE_1:1;
      SS is closed & i in NAT by A6,A7,TOPS_2:19,ORDINAL1:def 13; 
      then meet SS is closed & meet SS=R.i by A4,TOPS_2:29;
      hence thesis;
    end;
  let i;
  i in NAT by ORDINAL1:def 13;
  hence thesis by A4;
end;

theorem
  for M be non empty MetrSpace holds
    M is complete iff
       for F be Subset-Family of TopSpaceMetr M st F is closed & F is centered 
           & for r be Real st r > 0 
                ex A be Subset of M st A in F & A is bounded & diameter A < r
         holds meet F is non empty
proof
  let M be non empty MetrSpace;
  set T=TopSpaceMetr(M);
  thus M is complete implies
    for F be Subset-Family of T st F is closed & F is centered & for r st r>0 
        ex A be Subset of M st A in F & A is bounded & diameter A < r
      holds meet F is non empty
  proof
    assume 
  A1: M is complete;
    let F be Subset-Family of T such that 
  A2: F is closed & F is centered and 
  A3: for r st r>0 ex A be Subset of M st A in F & A is bounded & diameter A<r;
    defpred P[set,set] means
      for i st i=$1 for A be Subset of M st A=$2 holds
        A in F & A is bounded & diameter A <1/(i+1); 
  A4:for x st x in NAT ex y st y in bool(the carrier of M) & P[x,y]
      proof
        let x such that 
      A5: x in NAT;
        reconsider i=x as Element of NAT by A5;
        1/(i+1) > 0 by XREAL_1:141;
        then consider A be Subset of M such that
       A6: A in F & A is bounded & diameter A < 1/(i+1) by A3;
        take A;
        thus thesis by A6;
      end;
    consider f be SetSequence of M such that 
  A5: for x st x in NAT holds P[x,f.x] from FUNCT_2:sch 1(A4);
  A6:rng f c= F
      proof
        let x such that 
      A7: x in rng f;
        consider y such that
      A8: y in dom f & f.y=x by A7,FUNCT_1:def 5;
        reconsider y as Element of NAT by A8;
        f.y in F by A5;
        hence thesis by A8;
      end;
    consider R be SetSequence of T such that
  A7: R is descending and
  B6: F is centered implies R is non-empty and
      F is open implies R is open and 
  A8: F is closed implies R is closed and
  A9: for i holds R.i = meet {f.j where j is Element of NAT: j<=i} by A6,Th14;
    reconsider R'=R as non-empty SetSequence of M by A2,B6;
    now let i;    
       f.0 in {f.j where j is Element of NAT: j <= i} ;
       then meet {f.j where j is Element of NAT: j <= i} c= f.0 by SETFAM_1:4;
       then R.i c= f.0 & f.0 is bounded by A5,A9;
       hence R'.i is bounded by TBSP_1:21;
    end;
    then reconsider R' as non-empty bounded SetSequence of M by def1;
  A8':R' is closed & R' is descending by A7,A8,A2,Th8;
    deffunc F(Element of NAT)=1/(1+$1);
    consider seq be Real_Sequence such that 
  A10:for n be Element of NAT holds seq.n=F(n) from SEQ_1:sch 1;
    reconsider NULL=0 as Real;set Ns=NULL(#)seq;
    for n be Element of NAT holds seq.n=1/(n+1) by A10;then
  A11:seq is convergent & lim seq=0 by SEQ_4:45;then
  A12:Ns is convergent & lim Ns=NULL*0 by SEQ_2:21,22;
    set dR=diameter R';
    now let n be Element of NAT;
       set Sn={f.j where j is Element of NAT:j<=n};
       f.n in Sn & R.n=meet Sn by A9;
       then R.n c= f.n & f.n is bounded by A5,SETFAM_1:4;
       then diameter R'.n <= diameter f.n & diameter f.n < F(n)&R'.n is bounded 
         by A5,TBSP_1:21,32;
       then 0<= diameter R'.n & diameter R'.n <= F(n) & Ns.n=NULL*seq.n 
         & F(n)=seq.n & diameter R'.n=dR.n 
         by A10,XXREAL_0:2,TBSP_1:29,SEQ_1:13,def2;
       hence Ns.n <= dR.n & dR.n<=seq.n;
    end;then
  B1:dR is convergent & lim dR=0  by A11,A12,SEQ_2:33,34;
    then meet R'<>{} by A1,A8',Th11;
    then consider x0 be set such that
  A13:x0 in meet R' by XBOOLE_0:def 1;
    reconsider x0 as Point of M by A13;
  A14:now let y;
       assume 
    A15: y in F;
       then reconsider Y=y as Subset of T;
       defpred P'[set,set] means for i st i=$1 holds $2=R.i/\Y; 
    A16:for x st x in NAT ex z be set st z in bool(the carrier of M) & P'[x,z]
         proof
           let x such that 
         A17: x in NAT;
           reconsider i=x as Element of NAT by A17;
           take R.i/\Y;
           thus thesis;
         end;
       consider f' be SetSequence of M such that 
    A17: for x st x in NAT holds P'[x,f'.x] from FUNCT_2:sch 1(A16);
    A18:now let x such that 
       A19: x in dom f';
          reconsider i=x as Element of NAT by A19;
          set SS={f.j where j is Element of NAT:j<=i};
      A20':Y in {Y} & f.i in SS by TARSKI:def 1;
      A21:{Y}\/SS c= F
            proof
              let z be set such that 
          A22:z in {Y}\/SS;
              per cases by A22,XBOOLE_0:def 2;
                suppose z in {Y};
                  hence thesis by A15,TARSKI:def 1;end;
                suppose z in SS;
                  then ex j be Element of NAT st z=f.j & j<=i;
                  hence thesis by A5;end;
            end;
      A22:i+1 is finite;
          deffunc F(set)=f.$1;
      A23:{F(j)where j is Element of NAT:j in i+1} is finite 
            from FRAENKEL:sch 21(A22);
          SS c= {F(j) where j is Element of NAT:j in i+1}
            proof
              let x such that 
            A24: x in SS;
              consider j be Element of NAT such that
            A25: x=f.j & j<=i by A24;
              j<i+1 by A25,NAT_1:13;
              then j in i+1 by EULER_1:1;
              hence thesis by A25;
            end;
          then SS is finite by A23,FINSET_1:13;
          then {Y}\/SS is finite by FINSET_1:14;
          then meet({Y}\/SS)<>{} by A2,A21,COMPTS_1:def 2;
          then meet {Y} /\ meet SS <> {} by A20',SETFAM_1:10;
          then Y /\meet SS<>{} by SETFAM_1:11;
          then Y/\R.i<>{} by A9;
          hence f'.x is non empty by A17;
       end;
    A19:now let i;
          i in NAT by ORDINAL1:def 13;
          then  f'.i=R'.i /\ Y & R'.i is bounded & R.i /\ Y c= R.i
             by A17,def1,XBOOLE_1:17;
          hence f'.i is bounded by TBSP_1:21;
       end;
       now let i;
          reconsider Ri=R.i as Subset of T;
          R'.i is closed by A8',def8;         
          then Ri is closed & Y is closed & i in NAT
            by A2,A15,TOPS_2:def 2,Th7,ORDINAL1:def 13;
          then Ri/\Y is closed & f'.i=Ri/\Y by A17,TOPS_1:35;
          hence f'.i is closed by Th7;
       end;
       then reconsider f' as non-empty bounded closed SetSequence of M 
         by A18,A19,FUNCT_1:def 15,def1,def8;
       now let i be Element of NAT;
          f'.(i+1) =R.(i+1)/\Y & f'.i = R.i/\Y & R.(i+1) c= R.i 
            by A7,A17,KURATO_2:def 5;
          hence f'.(i+1) c= f'.i by XBOOLE_1:26;
       end;then
    A20:f' is descending by KURATO_2:def 5;
       set df=diameter f';
       now let n be Element of NAT;
          reconsider Y'=Y as Subset of M;
          R'.n is bounded & R.n/\Y c= R.n & R.n/\Y'=f'.n 
            by A17,def1,XBOOLE_1:17;
          then f'.n is bounded & diameter f'.n <= diameter R'.n 
            by TBSP_1:21,32;
          then 0<=diameter f'.n & diameter f'.n <= dR.n &
            Ns.n=NULL*seq.n by TBSP_1:29,def2,SEQ_1:13;
          hence Ns.n <= df.n & df.n<=dR.n by def2;
       end;
       then lim df=0  by A12,B1,SEQ_2:34;
       then meet f'<>{} by A1,A20,Th11;
       then consider z be set such that
    A21: z in meet f' by XBOOLE_0:def 1;
       reconsider z as Point of M by A21;
    A22: x0 = z
         proof
           assume x0<>z;
           then dist(x0,z)<>0 by METRIC_1:2;
           then dist(x0,z)>0 by METRIC_1:5;
           then consider i be Element of NAT such that
         A23: for j be Element of NAT st i<=j holds 
           abs(dR.j-0)<dist(x0,z) by B1,SEQ_2:def 7;
           z in f'.i & f'.i=R.i/\Y by A17,A21,KURATO_2:6;
           then z in R.i & x0 in R.i & R'.i is bounded 
             by A13,KURATO_2:6,def1,XBOOLE_0:def 3;
           then dist(x0,z)<=diameter (R'.i) & 0<=diameter (R'.i)
             by TBSP_1:def 10,29;
           then abs(diameter (R'.i))>=dist(x0,z) & abs(dR.i-0)<dist(x0,z) 
             by A23,ABSVALUE:def 1;
           hence thesis by def2;
         end;
       z in f'.0 & f'.0=R.0/\Y by A17,A21,KURATO_2:6;
       hence x0 in y by A22,XBOOLE_0:def 3;
    end;
    F<>{} by A2,COMPTS_1:def 2;
    hence thesis by A14,SETFAM_1:def 1;
  end;
  assume 
A1:for F be Subset-Family of T st F is closed & F is centered &
    for r st r > 0 ex A be Subset of M st A in F & A is bounded&diameter A<r
      holds meet F is non empty;
  now let S be non-empty bounded closed SetSequence of M such that
  A2: S is descending & lim diameter S = 0;
     reconsider RS=rng S as Subset-Family of T;
  A3:RS is closed & RS is centered by A2,Th12,Th13;
     now let r such that 
     A4: r > 0;
        set d=diameter S;
        d is bounded_below & d is non-increasing by A2,Th1,Th2;
        then d is convergent by SEQ_4:52;
        then consider n be Element of NAT such that 
     A5:  for m be Element of NAT st n<=m holds abs(d.m-0)<r 
          by A2,A4,SEQ_2:def 7;
        take Sn=S.n;
        Sn is bounded by def1;
        then abs(d.n-0)<r & d.n=diameter Sn & diameter Sn>=0 & dom S=NAT
          by A5,def2,TBSP_1:29,FUNCT_2:def 1;
        hence Sn in RS & Sn is bounded & diameter Sn <r 
          by ABSVALUE:def 1,FUNCT_1:def 5,def1;
     end;
     then meet RS is non empty by A1,A3;
     then consider x such that
   A4: x in meet RS by XBOOLE_0:def 1;
     now let i be Element of NAT;
        dom S=NAT by FUNCT_2:def 1;
        then RS<>{} & S.i in RS by RELAT_1:65,FUNCT_1:def 5;
        hence x in S.i by A4,SETFAM_1:def 1;
     end;
     hence meet S is non empty by KURATO_2:6;
  end;
  hence thesis by Th11;
end;

theorem Th16:
  for M be non empty MetrSpace,A be non empty Subset of M
    for B be Subset of M, B' be Subset of M|A st B = B' holds
      B' is bounded iff B is bounded
proof
  let M be non empty MetrSpace,A be non empty Subset of M;
  let B be Subset of M, B' be Subset of M|A such that 
A1: B = B';
  thus B' is bounded implies B is bounded
  proof
    assume 
  A2: B' is bounded;
    B' c= the carrier of (M|A);
    then B' c= A by TOPMETR:def 2;
    hence thesis by A1,A2,HAUSDORF:19;
  end;
  assume 
A2:B is bounded;
  per cases;
    suppose B'={}(M|A);
      hence thesis;end;
    suppose B'<>{}(M|A);
      then consider p be set such that
    A3: p in B' by XBOOLE_0:def 1;
      reconsider p as Point of (M|A) by A3;
      diameter B>=0 by A2,TBSP_1:29;then 
    A4:0+0 < diameter B+1 by XREAL_1:10;
      now let q be Point of (M|A) such that 
      A5: q in B';
         reconsider p'=p,q'=q as Point of M by TOPMETR:12;
      A6:dist(p,q) = dist(p',q') by TOPMETR:def 1;
         dist(p',q')<=diameter B & diameter B+0<=diameter B+1 
           by A1,A2,A3,A5,TBSP_1:def 10,XREAL_1:10;
         hence dist(p,q)<=diameter B+1 by A6,XXREAL_0:2;
      end;
      hence thesis by A3,A4,TBSP_1:15;end;
end;

theorem Th17:
  for M be non empty MetrSpace,A be non empty Subset of M
    for B be Subset of M, B' be Subset of M|A st B = B' & B is bounded holds
      diameter B' <= diameter B
proof
  let M be non empty MetrSpace,A be non empty Subset of M;
  let B be Subset of M, B' be Subset of M|A such that 
A1: B = B' & B is bounded;
A2:B' is bounded by A1,Th16;
  per cases;
    suppose B'={}(M|A);
      then diameter B'=0 & 0<=diameter B by A1,TBSP_1:def 10;
      hence thesis;end;
    suppose 
    A3: B'<>{}(M|A);    
      now let x,y be Point of (M|A) such that 
      A4: x in B' & y in B';
         reconsider x'=x,y'=y as Point of M by TOPMETR:12; 
         dist(x,y) = dist(x',y') by TOPMETR:def 1;
         hence dist(x,y)<=diameter B by A1,A4,TBSP_1:def 10;
      end;
      hence thesis by A2,A3,TBSP_1:def 10;end;
end;

theorem Th18:
  for M be non empty MetrSpace, A be non empty Subset of M
    for S be sequence of (M|A) holds S is sequence of M
proof
  let M be non empty MetrSpace, A be non empty Subset of M;
  let S be sequence of (M|A);
  A c= the carrier of M;
  then the carrier of (M|A) c= the carrier of M & 
    NAT<>{} by TOPMETR:def 2;
  hence thesis by FUNCT_2:9;
end;

theorem Th19:
  for M be non empty MetrSpace, A be non empty Subset of M
    for S be sequence of (M|A),S' be sequence of M st S = S' holds
      S' is Cauchy iff S is Cauchy
proof
  let M be non empty MetrSpace, A be non empty Subset of M;
  let S be sequence of (M|A),S' be sequence of M such that 
A1:S = S';
  thus S' is Cauchy implies S is Cauchy
    proof
      assume 
    A2: S' is Cauchy;
      let r such that 
    A3: r>0;
      consider p be Element of NAT such that 
    A4: for n,m be Element of NAT st p<=n & p<=m holds 
      dist(S'.n,S'.m)<r by A2,A3,TBSP_1:def 5;
      take p;
      let n,m be Element of NAT such that A5:p<=n & p<=m;
      dist(S.n,S.m) = dist(S'.n,S'.m) by A1,TOPMETR:def 1;
      hence thesis by A4,A5;
    end;
  assume 
A2: S is Cauchy;
  let r such that 
A3: r>0;
  consider p be Element of NAT such that 
A4: for n,m be Element of NAT st p<=n & p<=m holds 
      dist(S.n,S.m)<r by A2,A3,TBSP_1:def 5;
  take p;
  let n,m be Element of NAT such that 
A5: p <= n & p <= m;
  dist(S.n,S.m) = dist(S'.n,S'.m) by A1,TOPMETR:def 1;
  hence thesis by A4,A5;
end;
  
theorem
  for M be non empty MetrSpace st M is complete
    for A be non empty Subset of M, A' be Subset of TopSpaceMetr M st A = A'
      holds
    M|A is complete iff A' is closed
proof
  let M be non empty MetrSpace such that 
A1: M is complete;
  let A be non empty Subset of M, A' be Subset of TopSpaceMetr(M) such that 
A2: A = A';
  set MA=M|A;
  set TA=TopSpaceMetr(MA);set T=TopSpaceMetr(M);
  thus MA is complete implies A' is closed
    proof
      assume 
    A3: MA is complete;
    A4:Cl A' c= A'
        proof
          let p be set such that 
        A5: p in Cl A';
          reconsider p as Point of M by A5;
          defpred P[set,set] means
            for i st i=$1 holds $2=A /\ cl_Ball(p,1/(i+1));
        A6:for x st x in NAT ex y st y in bool(the carrier of MA) & P[x,y]
            proof
              let x such that 
        A7: x in NAT;
              reconsider i=x as Element of NAT by A7;
              take A/\cl_Ball(p,1/(i+1));
              A/\cl_Ball(p,1/(i+1)) c= A by XBOOLE_1:17;
              then A/\cl_Ball(p,1/(i+1)) c= the carrier of MA by TOPMETR:def 2;
              hence thesis;
            end;
          consider f be SetSequence of MA such that
        A7: for x st x in NAT holds P[x,f.x] from FUNCT_2:sch 1(A6);
        A8:now let x such that 
          A9: x in dom f;
             reconsider i=x as Element of NAT by A9;
             reconsider B=Ball(p,1/(i+1)) as Subset of T;
             Ball(p,1/(i+1)) in Family_open_set M & 1/(i+1)>0 
               by PCOMPS_1:33,XREAL_1:141;
             then B is open & p in B by PRE_TOPC:def 5,TBSP_1:16;
             then B meets A' by A5,PRE_TOPC:54;
             then consider y such that
          A10: y in B & y in A' by XBOOLE_0:3;
             reconsider y as Point of M by A10;
             dist(p,y)< 1/(i+1) by A10,METRIC_1:12;
             then y in cl_Ball(p,1/(i+1)) by METRIC_1:13;
             then y in A/\cl_Ball(p,1/(i+1)) by A2,A10,XBOOLE_0:def 3;
             hence f.x is non empty by A7;
          end;
        A9:now let i;
             set ACL=A/\cl_Ball(p,1/(i+1));
             cl_Ball(p,1/(i+1)) is bounded & ACL c= cl_Ball(p,1/(i+1))
               by Th5,XBOOLE_1:17;
             then A10:ACL is bounded by TBSP_1:21;
             i in NAT by ORDINAL1:def 13; 
             then f.i=ACL by A7;
             hence f.i is bounded by A10,Th16;
          end;
          now let i;
             reconsider cB=cl_Ball(p,1/(i+1)) as Subset of T;
             cB`=[#]M\cB & [#]M\cB in Family_open_set(M) by NAGATA_1:14;
             then cB` is open by PRE_TOPC:def 5;then
          A10:cB is closed by TOPS_1:29;             
             reconsider fi=f.i as Subset of TA;
          A11:TA=T|A' by A2,HAUSDORF:18;
             then [#](T|A')=A & i in NAT by TOPMETR:def 2,ORDINAL1:def 13;
             then fi=cB/\[#](T|A') by A7;
             then fi is closed by A10,A11,PRE_TOPC:43;             
             hence f.i is closed by Th7;
          end;
          then reconsider f as non-empty bounded closed SetSequence of MA
            by A8,A9,FUNCT_1:def 15,def1,def8;
          now let i be Element of NAT;set i1=i+1;
             cl_Ball(p,1/(i1+1)) c= cl_Ball(p,1/i1)
               proof
                 let x such that 
               A10: x in cl_Ball(p,1/(i1+1));
                 reconsider q=x as Point of M by A10;
                 i1<i1+1 by NAT_1:13;
                 then dist(p,q)<=1/(i1+1) & 1/(i1+1)<1/i1 
                   by XREAL_1:78,A10,METRIC_1:13;
                 then dist(p,q)<=1/i1 by XXREAL_0:2;
                 hence thesis by METRIC_1:13;
               end;
             then A/\cl_Ball(p,1/(i1+1)) c= A/\cl_Ball(p,1/i1) & 
               f.i=A/\cl_Ball(p,1/i1) by A7,XBOOLE_1:26;
             hence f.(i+1) c= f.i by A7;
          end;then
        A10:f is descending by KURATO_2:def 5;
          deffunc F(Element of NAT)=1/(1+$1);
          consider seq be Real_Sequence such that 
        A11:for n be Element of NAT holds seq.n=F(n) from SEQ_1:sch 1;
          reconsider NULL=0,TWO=2 as Real;
          set Ns=NULL(#)seq;set Ts=TWO(#)seq;
          for n be Element of NAT holds seq.n=1/(n+1) by A11;then
        A12':seq is convergent & lim seq=0 by SEQ_4:45;then
        A12:Ns is convergent & lim Ns=NULL*0 & Ts is convergent & lim Ts=TWO*0 
            by SEQ_2:21,22;
          set df=diameter f;
          now let n be Element of NAT;
             set cB=cl_Ball(p,1/(n+1));
          A13:cB is bounded & diameter cB <= 2*F(n) & A/\cB c= cB
               by Th6,Th5,XBOOLE_1:17;
             then A/\cB is bounded & diameter(A/\cB)<= diameter cB & f.n=A/\cB
               by A7,TBSP_1:21,32;
             then diameter(A/\cB)<=2*F(n) & diameter (f.n) <= diameter(A/\cB)& 
               f.n is bounded by Th17,A13,XXREAL_0:2,Th16;
             then  0<= diameter f.n & diameter f.n <= 2*F(n)&Ns.n=NULL*seq.n& 
               Ts.n=TWO*seq.n & F(n)=seq.n & diameter f.n=df.n 
               by A11,XXREAL_0:2,TBSP_1:29,SEQ_1:13,def2;
             hence Ns.n <= df.n & df.n<=Ts.n;
          end;
          then lim df = 0 & df is convergent by A12,SEQ_2:33,34;
          then meet f is non empty by A3,A10,Th11;
          then consider q be set such that
        A14:q in meet f by XBOOLE_0:def 1;
          reconsider q as Point of M by A14,TOPMETR:12;
          p = q
            proof
              assume p <> q;
              then dist(p,q)<>0 by METRIC_1:2;
              then dist(p,q)>0 by METRIC_1:5;
              then consider n be Element of NAT such that 
            A16:for m be Element of NAT st n<=m holds abs(seq.m-0)<dist(p,q) 
                by A12',SEQ_2:def 7;
              set cB=cl_Ball(p,1/(n+1));
              f.n = A/\cB & q in f.n & seq.n = F(n) & F(n) >= 0 
                by A11,A7,A14,KURATO_2:6;
              then q in cB & abs(seq.n-0)=F(n) 
                by XBOOLE_0:def 3,ABSVALUE:def 1;
              then dist(p,q) <= F(n) & F(n) < dist(p,q) by A16,METRIC_1:13;
              hence thesis;
            end;
          then f.0=A/\cl_Ball(p,1/(0+1)) & p in f.0 by A7,A14,KURATO_2:6;
          hence thesis by A2,XBOOLE_0:def 3;
        end;
      A' c= Cl A' by PRE_TOPC:48;
      hence thesis by A4,XBOOLE_0:def 10;
    end;
  assume 
A3: A' is closed;
  let S be sequence of MA such that 
A4: S is Cauchy;
  reconsider S'=S as sequence of M by Th18;
  S' is Cauchy by A4,Th19;then
A5: S' is convergent by A1,TBSP_1:def 6;
A6:the carrier of (M|A)=A' by A2,TOPMETR:def 2;
  now let n be Element of NAT;
     S.n in the carrier of (M|A);
     hence S'.n in A' by A2,TOPMETR:def 2;
  end;
  then reconsider limS=lim S' as Point of (M|A) by A6,A3,A5,TOPMETR3:2;
  take limS;
  let r such that 
A7:r>0; 
  consider n be Element of NAT such that 
A8: for m be Element of NAT st m>=n holds 
      dist(S'.m,lim S')<r by A5,A7,TBSP_1:def 4;
  take n;
  let m be Element of NAT such that 
A9: m>=n;
  dist(S.m,limS) = dist(S'.m,lim S') by TOPMETR:def 1;
  hence thesis by A8,A9;
end;

begin :: Countable compact spaces

definition let T be TopStruct;
  attr T is countably_compact means :DEF9:
   for F being Subset-Family of T st
     F is_a_cover_of T & F is open & F is countable
      ex G being Subset-Family of T
       st G c= F & G is_a_cover_of T & G is finite;
end;

theorem Th21:
  for T be TopStruct st T is compact holds T is countably_compact
proof
  let T be TopStruct such that 
A1: T is compact;
  let F being Subset-Family of T such that
A2: F is_a_cover_of T & F is open & F is countable;
  thus thesis by A1,A2,COMPTS_1:def 3;
end;

theorem Th22:
  for T being non empty TopSpace holds
   T is countably_compact iff
           for F being Subset-Family of T st 
               F is centered & F is closed & F is countable
             holds meet F <> {}
proof
  let T be non empty TopSpace;
  thus T is countably_compact implies
     for F be Subset-Family of T st F is centered &F is closed &F is countable
       holds meet F <> {}
    proof assume 
    A1:T is countably_compact;
      let F be Subset-Family of T such that
    A2:F is centered & F is closed and 
    A3:F is countable;assume
    A4:meet F = {};
      F <> {} by A2,COMPTS_1:def 2;
      then union COMPLEMENT(F) = (meet F)` by TOPS_2:12
                              .= [#] T by A4;
      then COMPLEMENT(F) is_a_cover_of T & COMPLEMENT(F) is open & 
       COMPLEMENT(F) is countable by A3,TOPGEN_4:1,PRE_TOPC:def 8,A2,TOPS_2:16;
      then consider G' be Subset-Family of T such that
    A5:G' c= COMPLEMENT(F) & G' is_a_cover_of T and 
    A6:G' is finite by A1,DEF9;
    A7:COMPLEMENT(G') c= F
        proof
          let x such that 
        A8:x in COMPLEMENT(G');
          reconsider x'=x as Subset of T by A8;
          x'` in G' by A8,SETFAM_1:def 8;
          then x'`` in F by A5,SETFAM_1:def 8;
          hence thesis;
        end;
    A8:G' <> {} by A5,TOPS_2:5;then
    A9:meet COMPLEMENT(G') = (union G')` by TOPS_2:11
                          .= ([#] T) \ ([#] T) by A5,PRE_TOPC:def 8
                          .= {} by XBOOLE_1:37;
      COMPLEMENT(G') <> {} & COMPLEMENT(G') is finite 
        by A6,A8,TOPS_2:10,13;
      hence contradiction by A2,A7,A9,COMPTS_1:def 2;
    end;
  assume 
A1:for F being Subset-Family of T st
     F is centered & F is closed & F is countable holds meet F <> {};
  let F be Subset-Family of T such that
A2: F is_a_cover_of T & F is open and 
A3: F is countable;
A4:COMPLEMENT(F) is countable & COMPLEMENT(F) is closed &
     F <> {} by A2,A3,TOPS_2:5,17,TOPGEN_4:1;
  then  meet COMPLEMENT(F) = (union F)` by TOPS_2:11
                          .= ([#] T) \ ([#] T) by A2,PRE_TOPC:def 8
                          .= {} by XBOOLE_1:37;
  then COMPLEMENT(F) <> {} & not COMPLEMENT(F) is centered 
    by A1,A4,TOPS_2:10;
  then consider G' being set such that
A5: G' <> {} & G' c= COMPLEMENT(F) and 
A6: G' is finite & meet G' = {} by COMPTS_1:def 2;
  reconsider G' as Subset-Family of T by A5,XBOOLE_1:1;
  take F'=COMPLEMENT(G');
  thus F' c= F
    proof
      let x such that 
    A7: x in F';
      reconsider x'=x as Subset of T by A7;
      x'` in G' by A7,SETFAM_1:def 8;
      then x'`` in F by A5,SETFAM_1:def 8;
      hence x in F;
    end;
  union F' = (meet G')` by A5,TOPS_2:12
          .= [#] T by A6;
  hence thesis by A6,TOPS_2:13,PRE_TOPC:def 8;
end;

theorem Th23:
  for T being non empty TopSpace holds
    T is countably_compact iff
           for S be non-empty closed SetSequence of T st S is descending
             holds meet S <> {}
proof
  let T being non empty TopSpace;
  thus T is countably_compact implies
    for S be non-empty closed SetSequence of T st 
      S is descending holds meet S <> {}
    proof assume
    A1:T is countably_compact;
      let S be non-empty closed SetSequence of T such that 
    A2: S is descending;
      reconsider rngS=rng S as Subset-Family of T;
      dom S=NAT by FUNCT_2:def 1;then
    A4:rngS is centered & rngS is countable by A2,Th12,CARD_4:45;
      now let D be Subset of T such that 
      A5: D in rngS;
         consider x such that
      A6:  x in dom S & S.x=D by A5,FUNCT_1:def 5;
         reconsider x as Element of NAT by A6;
         S.x is closed by def6;
         hence D is closed by A6;
      end;
      then rngS is closed by TOPS_2:def 2;
      then meet rngS<>{} by A1,A4,Th22;
      then consider x such that
    A5: x in meet rngS by XBOOLE_0:def 1;
      now let n be Element of NAT;
         dom S=NAT by FUNCT_2:def 1;
         then S.n in rngS by FUNCT_1:def 5;
         hence x in S.n by A5,SETFAM_1:def 1;
      end;
      hence thesis by KURATO_2:6;
    end;
  assume 
A1: for S be non-empty closed SetSequence of T st 
      S is descending holds meet S <> {};
  now let F be Subset-Family of T such that
A2: F is centered & F is closed and 
A3: F is countable;
A4: Card F <=` alef 0 by A3,CARD_4:def 1;
     now per cases by A4,CARD_1:13;
        suppose Card F = alef 0;
          then NAT,F are_equipotent by CARD_1:21,38;
          then consider s be Function such that
        A5: s is one-to-one & dom s = NAT & rng s = F by WELLORD2:def 4;
          reconsider s as SetSequence of T by A5,FUNCT_2:4;
          consider R be SetSequence of T such that
        A6: R is descending and
        A7: F is centered implies R is non-empty and
            F is open implies R is open  and  
        A8: F is closed implies R is closed  and
        A9: for i holds R.i=meet{s.j where j is Element of NAT:j<=i}by A5,Th14;
          meet R<>{} by A1,A2,A6,A7,A8;
          then consider x such that
        A10:x in meet R by XBOOLE_0:def 1;
        A11:F is non empty by A5,RELAT_1:65;
          now let y; 
             assume y in F;
             then consider z be set such that
          A12: z in dom s & s.z=y by A5,FUNCT_1:def 5;
             reconsider z as Element of NAT by A12;
             s.z in {s.j where j is Element of NAT:j<=z} &
             R.z=meet {s.j where j is Element of NAT:j<=z} by A9;
             then R.z c= s.z & x in R.z by A10,SETFAM_1:4,KURATO_2:6;
             hence x in y by A12;
          end;
          hence meet F is non empty by A11,SETFAM_1:def 1;end;
        suppose Card F <` alef 0;
          then F is finite &  F<>{} by CARD_4:2,A2,COMPTS_1:def 2;
          hence meet F is non empty by A2,COMPTS_1:def 2;end;
     end;
     hence meet F<>{};
  end;
  hence thesis by Th22;
end;

theorem Th24:
  for T being non empty TopSpace
    for F be Subset-Family of T
      for S be SetSequence of T st rng S c= F & S is non-empty
        ex R be non-empty closed SetSequence of T st 
           R is descending &
           ( F is locally_finite & S is one-to-one implies meet R = {} ) &
           for i ex Si be Subset-Family of T st 
             R.i = Cl union Si &
             Si = {S.j where j is Element of NAT: j >= i}
proof
  let T being non empty TopSpace;
  let F be Subset-Family of T;
  let S be SetSequence of T such that 
A2: rng S c= F & S is non-empty;  
  defpred r[set,set] means 
    for i st i=$1 ex SS be Subset-Family of T st SS c= F &
      SS = {S.j where j is Element of NAT:j >= i} & $2=Cl(union SS);
A3:for x st x in NAT ex y st y in bool(the carrier of T) & r[x,y]
    proof
      let x such that 
    A4: x in NAT;
      reconsider x'=x as Element of NAT by A4;
      set SS={S.j where j is Element of NAT:j >= x'};
      SS c= bool(the carrier of T)
        proof
          let y such that 
        A5: y in SS;
          ex j be Element of NAT st S.j=y & j>=x' by A5;
          hence thesis;
        end;
      then reconsider SS as Subset-Family of T;      
      take Cl union SS;
      SS c= F
        proof
          let y such that 
        A5: y in SS;
          consider j be Element of NAT such that 
        A6: S.j=y & j>=x' by A5;
          dom S=NAT by FUNCT_2:def 1; 
          then y in rng S by A6,FUNCT_1:def 5;
          hence thesis by A2;
        end;
      hence thesis;
    end;
  consider R be SetSequence of T such that
A4: for x st x in NAT holds r[x,R.x] from FUNCT_2:sch 1(A3);
A5:now let n be set such that 
  B6: n in dom R;
     reconsider n'=n as Element of NAT by B6;
     consider SS be Subset-Family of T such that 
       SS c= F and
  A6:  SS = {S.j where j is Element of NAT:j>=n'} & R.n'=Cl(union SS) by A4;
     dom S=NAT by FUNCT_2:def 1;then
  A7:S.n'<>{} by A2,FUNCT_1:def 15;
     S.n' in SS by A6;
     then S.n' c= union SS by ZFMISC_1:92;
     then S.n' c= Cl(S.n') & Cl(S.n') c= Cl(union SS) by PRE_TOPC:48,49;
     then S.n' c= Cl (union SS) by XBOOLE_1:1;
     hence R.n is non empty by A6,A7,XBOOLE_1:3;
  end;
  now let n;
     reconsider n'=n as Element of NAT by ORDINAL1:def 13;
     ex SS be Subset-Family of T st 
       SS c= F &
       SS = {S.j where j is Element of NAT:j>=n'} & R.n'=Cl(union SS) by A4;
     hence R.n is closed;
  end;
  then reconsider R as non-empty closed SetSequence of T 
    by A5,FUNCT_1:def 15,def6;
  take R;
  now let n be Element of NAT;
     consider Sn be Subset-Family of T such that 
       Sn c= F and
  A7:  Sn = {S.j where j is Element of NAT:j>=n} and
  A8:  R.n=Cl(union Sn) by A4;
     consider Sn1 be Subset-Family of T such that 
       Sn1 c= F and
  A9:  Sn1 = {S.j where j is Element of NAT:j>=n+1} and
  A10: R.(n+1)=Cl(union Sn1) by A4;
     Sn1 c= Sn
       proof
         let y such that 
       A11: y in Sn1;
         consider j be Element of NAT such that
       A12:y=S.j & j>=n+1  by A9,A11;
         j>=n by A12,NAT_1:13;
         hence thesis by A7,A12;
       end;
     then union Sn1 c= union Sn by ZFMISC_1:95;
     hence R.(n+1) c= R.n by A8,A10,PRE_TOPC:49;
  end;
  hence R is descending by KURATO_2:def 5;
  thus F is locally_finite & S is one-to-one implies meet R = {} 
    proof
      assume 
    A6: F is locally_finite & S is one-to-one;
      assume meet R <> {};
      then consider x such that
    A7: x in meet R by XBOOLE_0:def 1;
      reconsider x as Point of T by A7; 
    A8:dom S=NAT by FUNCT_2:def 1;
      then reconsider rngS=rng S as non empty Subset-Family of T by RELAT_1:65;
      rng S is locally_finite by A2,A6,PCOMPS_1:12;
      then consider W be Subset of T such that 
    A9: x in W & W is open and
    A10:{ V where V is Subset of T: V in rngS & V meets W } is finite 
        by PCOMPS_1:def 2;
      reconsider S as Function of NAT,rngS by A8,FUNCT_2:3;
      reconsider S'=S" as Function;
      reconsider S' as Function of rngS,NAT by A6,FUNCT_2:31;
      deffunc s'(Element of rngS)=S'.$1;
      set X={ V where V is Subset of T: V in rngS & V meets W };
      set Y={s'(z) where z is Element of rngS:z in X};
    A11:Y is finite from FRAENKEL:sch 21(A10);
      Y c= NAT
        proof
          let y such that 
        A12:y in Y;
          ex z be Element of rngS st
        y =s'(z) & z in X by A12;
          hence thesis;
        end;
      then reconsider Y as Subset of NAT;
      consider n be Element of NAT such that
    A12:for k be Element of NAT st k in Y holds k <= n by A11,STIRL2_1:66;
      set n1=n+1;
      consider Sn be Subset-Family of T such that 
    A13:Sn c= F and
    A14:Sn ={S.j where j is Element of NAT:j>=n1} and
    A15:R.n1=Cl(union Sn) by A4;
      Sn is locally_finite by A6,A13,PCOMPS_1:12;
      then Cl(union Sn)=union(clf Sn) & x in R.n1 by A7,KURATO_2:6,PCOMPS_1:23;
      then consider CLF be set such that
    A16:x in CLF & CLF in clf Sn by A15,TARSKI:def 4;
      reconsider CLF as Subset of T by A16;
      consider U be Subset of T such that
    A17:CLF = Cl U & U in Sn by A16,PCOMPS_1:def 3;
      consider j be Element of NAT such that
    A18:U=S.j & j>=n1 by A14,A17;
      S.j in rngS & S.j meets W by A9,A16,A17,A18,TOPS_1:39;
      then S.j in X & (S").(S.j) = j by A6,FUNCT_2:32;
      then j in Y;
      then j <=n by A12; 
      hence thesis by A18,NAT_1:13;
    end;
  let i;
  i in NAT by ORDINAL1:def 13;
  then ex SS be Subset-Family of T st SS c= F &
    SS = {S.j where j is Element of NAT:j >= i} & R.i=Cl(union SS) by A4;
  hence thesis;
end;

LM1to2:
  for T being non empty TopSpace st T is countably_compact
    for F be Subset-Family of T st 
      F is locally_finite & F is with_non-empty_elements
    holds F is finite
proof
  let T be non empty TopSpace such that A0:T is countably_compact;
  given F be Subset-Family of T such that
A1: F is locally_finite and 
A2: F is with_non-empty_elements and 
A3: F is infinite;
  consider f be Function of NAT, F such that 
A4: f is one-to-one by A3,DICKSON:3;
A5: rng f c= F;
  reconsider f as SetSequence of T by A3,FUNCT_2:9;
  now let x such that 
  A7: x in dom f;
    f.x in rng f by A7,FUNCT_1:def 5;
    hence f.x is non empty by A2,A5,SETFAM_1:def 9;
  end;
  then f is non-empty by FUNCT_1:def 15;
  then ex R be non-empty closed SetSequence of T st
 R is descending &
( F is locally_finite & f is one-to-one implies meet R = {})&
    for i ex fi be Subset-Family of T st
      R.i = Cl union fi & fi = {f.j where j is Element of NAT: j >= i} 
      by Th24,A5;
   hence thesis by A0,A1,A4,Th23;
end;

LM2to3:
  for T be non empty TopSpace st
       for F be Subset-Family of T st 
         F is locally_finite & F is with_non-empty_elements holds F is finite
    for F be Subset-Family of T st F is locally_finite & 
         for A be Subset of T st A in F holds Card A = 1
       holds F is finite
proof
  let T be non empty TopSpace such that
A1: for F be Subset-Family of T st 
      F is locally_finite & F is with_non-empty_elements holds F is finite;
  let F be Subset-Family of T such that 
A2: F is locally_finite and
A3: for A be Subset of T st A in F holds Card A = 1;
  not {}T in F by A3,CARD_1:78;
  then F is with_non-empty_elements by SETFAM_1:def 9;
  hence thesis by A1,A2;
end;

LM3to4:
  for T be non empty TopSpace st
      for F be Subset-Family of T st F is locally_finite & 
         for A be Subset of T st A in F holds Card A = 1
        holds F is finite
    for A be Subset of T st A is infinite holds Der A is non empty
proof
  let T be non empty TopSpace such that
A1: for F be Subset-Family of T st F is locally_finite & 
      for A be Subset of T st A in F holds Card A = 1 holds F is finite;
  let A be Subset of T such that A2:A is infinite;
  assume 
A3: Der A is empty;
  set F={{x} where x is Element of T: x in A};
  reconsider F as Subset-Family of T by RELSET_2:16;
A4:F is locally_finite 
    proof 
      let x be Point of T;
      consider U be open Subset of T such that 
    A5: x in U and
    A6: for y being Point of T st y in A /\ U holds x = y by A3,TOPGEN_1:19;
      take U;
      set M={ V where V is Subset of T: V in F & V meets U};
      M c= {{x}}
        proof
          let v be set such that 
        A7: v in M;
          consider V be Subset of T such that 
        A8: v=V & V in F & V meets U by A7;
          consider y be Point of T such that
        A9: V = {y} & y in A by A8;
          y in U by A8,A9,ZFMISC_1:56;
          then y in A/\U & {x} in {{x}} by TARSKI:def 1,A9,XBOOLE_0:def 3;
          hence thesis by A6,A8,A9;
        end;
      hence thesis by A5,FINSET_1:13;
    end;
  now let a be Subset of T such that 
  A5: a in F;
     ex y be Point of T st a={y} & y in A by A5;
     hence Card a = 1 by CARD_1:50;
  end;then 
A5: F is finite by A1,A4;
  deffunc P(set)=meet $1;
  set PP={P(y) where y is Element of bool(the carrier of T):y in F};
A6: PP is finite from FRAENKEL:sch 21(A5);
  A c= PP
    proof
      let y such that 
    A7: y in A; 
      reconsider y'=y as Point of T by A7;
      {y'} in F & {y'} is Subset of T by A7;
      then P({y'}) in PP;
      hence thesis by SETFAM_1:11;
    end;
  hence thesis by A2,A6,FINSET_1:13;
end;
  
theorem Th25:
  for F be Function st dom F is infinite & rng F is finite
    ex x st x in rng F & F"{x} is infinite
proof
  let F be Function such that 
A1: dom F is infinite & rng F is finite;
  assume 
A2: for x st x in rng F holds F"{x} is finite;
  deffunc f(set)=F"{$1};
  consider g be Function such that
A3: dom g = rng F & for x st x in rng F holds g.x = f(x) from FUNCT_1:sch 3;
  now let x such that 
  A4: x in dom g;
     g.x=F"{x} by A3,A4;
     hence g.x is finite by A2,A3,A4;
  end;then 
A4: Union g is finite by A1,A3,CARD_4:63;
A5:dom F c= Union g
   proof
     let x such that 
   A6: x in dom F;
      F.x in {F.x} & F.x in rng F by A6,TARSKI:def 1,FUNCT_1:def 5;
      then x in F"{F.x} & g.(F.x)=F"{F.x} & g.(F.x) in rng g 
        by A3,A6,FUNCT_1:def 5,def 13;
      then x in union rng g by TARSKI:def 4;
      hence thesis by CARD_3:def 4;
    end;
  Union g c= dom F
    proof
      let x such that 
    A6: x in Union g;
      x in union rng g by A6,CARD_3:def 4;
      then consider y such that
    A7: x in y & y in rng g by TARSKI:def 4;
      consider z be set such that
    A8: z in dom g & y=g.z by A7,FUNCT_1:def 5;
      y=F"{z} by A3,A8;
      hence thesis by A7,FUNCT_1:def 13;
    end;
  hence thesis by A1,A4,A5,XBOOLE_0:def 10;
end;

theorem Th26:
  for X be non empty set, F be SetSequence of X st F is descending
    for S be Function of NAT,X st for n holds S.n in F.n holds
      rng S is finite implies meet F is non empty
proof
  let X be non empty set, F be SetSequence of X such that 
A1: F is descending;
  let S be Function of NAT,X such that 
A2: for n holds S.n in F.n;
  assume 
A3: rng S is finite;
  dom S=NAT & NAT is infinite by FUNCT_2:def 1,CARD_4:15;
  then consider x such that 
A5: x in rng S & S"{x} is infinite by A3,Th25;
  now let n be Element of NAT;
     ex i st x in F.i & i >= n
       proof
         assume 
       A6: for i st x in F.i holds i<n;        
         S"{x} c= n
           proof
             let y such that 
           A8: y in S"{x};
             reconsider i=y as Element of NAT by A8;
             S.i in {x} by A8,FUNCT_1:def 13;
             then S.i=x & S.i in F.i by A2,TARSKI:def 1;
             then i<n by A6;
             hence thesis by EULER_1:1;
           end;
         hence thesis by A5,FINSET_1:13;
       end;
     then consider i such that 
  A6:  x in F.i & i>=n;
     i in NAT by ORDINAL1:def 13;
     then F.i c= F.n by A1,A6,KURATO_2:22;
     hence x in F.n by A6;
  end;
  hence thesis by KURATO_2:6;
end;

LM5to1:
  for T be being_T1 non empty TopSpace st
    for A be Subset of T st A is infinite countable holds Der A is non empty
    holds T is countably_compact
proof
  let T be being_T1 non empty TopSpace such that
A1: for A be Subset of T st A is infinite countable holds 
                                                       Der A is non empty;
  assume not T is countably_compact;
  then consider S be non-empty closed SetSequence of T such that 
A2: S is descending & meet S = {} by Th23;
  defpred P[set,set] means $2 in S.$1; 
A3:for x st x in NAT ex y st y in the carrier of T & P[x,y]
    proof
      let x such that 
    A4: x in NAT;
      reconsider x'=x as Element of NAT by A4;
      dom S=NAT by FUNCT_2:def 1;
      then S.x' is non empty by FUNCT_1:def 15;
      then consider y such that
    A5: y in S.x' by XBOOLE_0:def 1;
      take y;
      thus thesis by A5;
    end;
  consider F be sequence of T such that
A4: for x st x in NAT holds P[x,F.x] from FUNCT_2:sch 1(A3);
  reconsider rngF=rng F as Subset of T;
  now let n;
     n in NAT by ORDINAL1:def 13;
     hence F.n in S.n by A4;
  end;then 
A5:rng F is infinite by A2,Th26; 
  dom F=NAT by FUNCT_2:def 1;
  then rng F is countable by CARD_4:45;
  then Der rngF is non empty by A1,A5;
  then consider p be set such that
A6: p in Der rngF by XBOOLE_0:def 1;
  reconsider p as Point of T by A6;
  consider n be Element of NAT such that
A7: not p in S.n by A2,KURATO_2:6;
  deffunc f(set)=F.$1;
  set F1n={f(i) where i is Element of NAT:i in n+1};
A8:n+1 is finite;
A9:F1n is finite from FRAENKEL:sch 21(A8);
  F1n c= the carrier of T
    proof
      let x such that 
    A10:x in F1n;
      ex i be Element of NAT st x=F.i & i in n+1 by A10;   
      hence thesis;
    end;
  then reconsider F1n as Subset of T;
  set U=((S.n)`)\(F1n\{p});
  reconsider U as Subset of T;
  F1n\{p}c=F1n by XBOOLE_1:36;
  then  F1n\{p} is finite & (S.n) is closed by A9,FINSET_1:13,def6;
  then F1n\{p} is closed & (S.n)` is open by YELLOW13:1,TOPS_1:29;then
A10:U is open by FRECHET:4;
  p in {p} by TARSKI:def 1;
  then not p in F1n\{p} & p in (S.n)` by A7,XBOOLE_0:def 4;
  then p in U by XBOOLE_0:def 4;
  then consider q be Point of T such that
A11: q in rngF /\ U & q <> p by A6,A10,TOPGEN_1:19;
  q in rngF by A11,XBOOLE_0:def 3;
  then consider i be set such that
A12: i in dom F & F.i=q by FUNCT_1:def 5;
  reconsider i as Element of NAT by A12;
  per cases;
    suppose i<=n;
      then i < n+1 by NAT_1:13;
      then i in n+1 by EULER_1:1;
      then q in F1n by A12;
      then q in F1n\{p} by A11,ZFMISC_1:64;
      then not q in U by XBOOLE_0:def 4;
      hence contradiction by A11,XBOOLE_0:def 3;end;
  suppose i>n;
    then q in S.i & S.i c= S.n by A2,A4,A12,KURATO_2:22;
    then not q in (S.n)` by XBOOLE_0:def 4;
    then not q in U by XBOOLE_0:def 4;
    hence contradiction by A11,XBOOLE_0:def 3;end;
end;

LM3to1:
  for T being non empty TopSpace st 
     for F be Subset-Family of T st F is locally_finite & 
          for A be Subset of T st A in F holds Card A = 1
       holds F is finite
  holds T is countably_compact
proof
  let T being non empty TopSpace such that
A1: for F be Subset-Family of T st F is locally_finite & 
        for A be Subset of T st A in F holds Card A = 1
      holds F is finite;
  assume not T is countably_compact;
  then consider S be non-empty closed SetSequence of T such that 
A2: S is descending & meet S = {} by Th23;
  defpred P[set,set] means $2 in S.$1; 
A3:for x st x in NAT ex y st y in the carrier of T & P[x,y]
    proof
      let x such that 
    A4: x in NAT;
      reconsider x'=x as Element of NAT by A4;
      dom S=NAT by FUNCT_2:def 1;
      then S.x' is non empty by FUNCT_1:def 15;
      then consider y such that
    A5: y in S.x' by XBOOLE_0:def 1;
      take y;
      thus thesis by A5;
    end;
  consider F be sequence of T such that
A4: for x st x in NAT holds P[x,F.x] from FUNCT_2:sch 1(A3);
  reconsider rngF=rng F as Subset of T;
  now let n;
    n in NAT by ORDINAL1:def 13;
    hence F.n in S.n by A4;
  end;then 
A5:rng F is infinite by A2,Th26; 
  reconsider rngF=rng F as Subset of T;
  set A={{x} where x is Element of T: x in rngF};
  reconsider A as Subset-Family of T by RELSET_2:16;
A6:A is locally_finite
  proof
    let x be Point of T;
    consider i be Element of NAT such that
  A7: not x in S.i by A2,KURATO_2:6;
    take Si'=(S.i)`;
    S.i is closed by def6;
    hence  x in Si' & Si' is open by A7,TOPS_1:29,SUBSET_1:50;
    deffunc f(set)={F.$1};
  A8:i is finite;
    set SI={f(j) where j is Element of NAT:j in i};
  A9:SI is finite from FRAENKEL:sch 21(A8);
    set meetS={ V where V is Subset of T: V in A & V meets Si' };
    meetS c= SI
      proof
        let v be set such that 
      A10: v in meetS;
        consider V be Subset of T such that 
      A11:V=v & V in A & V meets Si' by A10;
       consider y be Point of T such that
      A12:V={y} & y in rng F by A11;
       consider z be set such that
      A13:z in dom F & y=F.z by A12,FUNCT_1:def 5;
        reconsider z as Element of NAT by A13;
        z in i
           proof
            assume not z in i;
            then z>=i by EULER_1:1;
            then y in S.z & S.z c= S.i by A2,A4,A13,KURATO_2:22; 
            then y in S.i & y in Si' by A11,A12,ZFMISC_1:56;
            hence thesis by XBOOLE_0:def 4;
          end;
        hence thesis by A11,A12,A13; 
      end;
    hence meetS is finite by A9,FINSET_1:13; 
  end;
  now let a be Subset of T such that 
  A7: a in A;
     ex y be Point of T st a={y} & y in rngF by A7;
     hence Card a = 1 by CARD_1:50;
  end;then 
A7: A is finite by A1,A6;
  deffunc P(set)=meet $1;
  set PP={P(y) where y is Element of bool(the carrier of T):y in A};
A8:PP is finite from FRAENKEL:sch 21(A7);
  rngF c= PP
    proof
      let y such that 
    A9: y in rngF; 
      reconsider y'=y as Point of T by A9;
      {y'} in A & {y'} is Subset of T by A9;
      then P({y'}) in PP;
      hence thesis by SETFAM_1:11;
    end;
   hence thesis by A5,A8,FINSET_1:13;
end;

theorem Th27:
  for T be non empty TopSpace holds    
    T is countably_compact iff 
                 for F be Subset-Family of T st 
                      F is locally_finite & F is with_non-empty_elements
                   holds F is finite
proof
  let T be non empty TopSpace;    
  thus T is countably_compact implies 
                for F be Subset-Family of T st 
                     F is locally_finite & F is with_non-empty_elements 
                  holds F is finite by LM1to2;
  assume for F be Subset-Family of T st 
             F is locally_finite & F is with_non-empty_elements
           holds F is finite;
  then for F be Subset-Family of T st 
           F is locally_finite & 
           for A be Subset of T st A in F holds Card A = 1
         holds F is finite by LM2to3;
  hence thesis by LM3to1;
end;

theorem Th28:
  for T be non empty TopSpace holds
    T is countably_compact iff
          for F be Subset-Family of T st F is locally_finite &
                for A be Subset of T st A in F holds Card A = 1
            holds F is finite
proof
  let T be non empty TopSpace;
  thus T is countably_compact implies 
          for F be Subset-Family of T st F is locally_finite & 
                for A be Subset of T st A in F holds Card A=1
            holds F is finite 
   proof
     assume T is countably_compact;
     then for F be Subset-Family of T st 
               F is locally_finite & F is with_non-empty_elements
             holds F is finite by Th27;
     hence thesis by LM2to3;
   end;
   thus thesis by LM3to1;
end;

theorem Th29:
  for T be being_T1 non empty TopSpace holds
    T is countably_compact iff
          for A be Subset of T st A is infinite holds Der A is non empty
proof
  let T be being_T1 non empty TopSpace;
  thus T is countably_compact implies 
                for A be Subset of T st A is infinite holds Der A is non empty
    proof
      assume T is countably_compact;
      then for F be Subset-Family of T st F is locally_finite & 
               for A be Subset of T st A in F holds Card A=1
             holds F is finite by Th28;
      hence thesis by LM3to4;
    end;
  assume for A be Subset of T st A is infinite holds Der A is non empty;
  then for A be Subset of T st A is infinite countable holds 
                                                           Der A is non empty;
  hence thesis by LM5to1;  
end;

theorem
  for T be being_T1 non empty TopSpace holds
    T is countably_compact iff
          for A be Subset of T st A is infinite countable holds
       Der A is non empty by Th29,LM5to1;

scheme Th39{X()->non empty set,P[set,set]}:
ex A be Subset of X() st 
  ( for x,y be Element of X() st x in A & y in A & x <> y holds P[x,y] ) &
     for x be Element of X() ex y be Element of X() st y in A & not P[x,y]
provided
  A1:for x,y be Element of X() holds P[x,y] iff P[y,x] 
  and
  A2:for x be Element of X() holds not P[x,x]       
proof
  set bX=bool X();
  consider R be Relation such that 
A3: R well_orders X() by WELLORD2:26;
  R/\[:X(),X():]c=[:X(),X():] & R/\[:X(),X():]=R|_2 X() 
    by WELLORD1:def 6,XBOOLE_1:17;
  then reconsider R2=R |_2 X() as Relation of X() by RELSET_1:def 1;
  reconsider RS=RelStr(#X(),R2#) as non empty RelStr;
A4:R2 well_orders X() & field R2 = X() by A3,PCOMPS_2:5; then 
A5:R2 is_well_founded_in X() & R2 is well-ordering 
  by WELLORD1:def 5,WELLORD1:8;then 
A6:RS is well_founded by WELLFND1:def 2;
  set cRS=the carrier of RS;
  set IRS=the InternalRel of RS;
  defpred H[set,set,set] means
    for p be Element of X(), f be PartFunc of cRS,bX st 
      $1=p & $2=f holds
      ( (for q be Element of X() st q in union(rng f) holds P[p,q])
          implies $3=union (rng f) \/ {p} ) &
      ( (ex q be Element of X() st q in union (rng f) & not P[p,q])
          implies $3=union (rng f) );
 A7:for x,y st x in cRS & y in PFuncs(cRS, bX) 
    ex z be set st z in bX & H[x,y,z]
    proof
      let x,y such that 
    A8: x in cRS & y in PFuncs(cRS, bX);
      reconsider p=x as Element of X() by A8;
      reconsider f=y as PartFunc of cRS,bX by A8,PARTFUN1:120;
      per cases;
       suppose A9:for q be Element of X() st q in union(rng f) holds P[p,q];
         take U=union (rng f) \/ {p};
         thus thesis by A9;end;
       suppose A9:ex q be Element of X() st q in union (rng f) & not P[p,q];
         take U=union (rng f);
         thus thesis by A9;end;  
    end;
  consider h be Function of [:cRS,PFuncs(cRS, bX):],bX such that
 A8:for x,y st x in cRS & y in PFuncs(cRS, bX) holds H[x,y,h.(x,y)]
      from BINOP_1:sch 1(A7);
  consider f be Function of cRS, bX such that
 A9:f is_recursively_expressed_by h by A6,WELLFND1:12;
  reconsider rngf=rng f as Subset of bX;
  take A=union rngf;
  defpred S[set] means
    f.$1 c= (IRS-Seg $1)\/{$1} & 
    ($1 in f.$1 implies 
      for r be Element of X() st r in union(rng (f|IRS-Seg $1)) holds P[$1,r])&
    (not $1 in f.$1 implies 
      ex r be Element of X() st r in union(rng (f|IRS-Seg $1)) & not P[$1,r]);
A10:for x be Element of RS st
     for y be Element of RS st y <> x & [y,x] in IRS holds S[y] holds S[x]
     proof
       let x be Element of RS such that
     A11: for y be Element of RS st y <> x & [y,x] in IRS holds S[y];
       set fIx=f|IRS-Seg x;
     A12:union rng fIx c= IRS-Seg x
         proof
           let y be set such that 
         A13: y in union rng fIx;
           consider z be set such that
         A14: y in z & z in rng fIx by A13,TARSKI:def 4;
           consider t be set such that
         A15: t in dom fIx & fIx.t=z by A14,FUNCT_1:def 5;
         A16:t in IRS-Seg x & IRS-Seg x c= cRS by A15,RELAT_1:86,WELLFND1:4;
           reconsider t as Element of RS by A15;
           t<>x & [t,x] in IRS by A16,WELLORD1:def 1;
           then f.t c= (IRS-Seg t)\/{t} & fIx.t=f.t & IRS-Seg(t)c=IRS-Seg(x) &
             {t} c= IRS-Seg(x) 
             by A4,A5,A11,A15,A16,FUNCT_1:70,WELLORD1:37,ZFMISC_1:37;
           then y in (IRS-Seg t)\/{t} & (IRS-Seg t)\/{t} c= IRS-Seg(x) 
             by A14,A15,XBOOLE_1:8;
           hence thesis;
         end;
     A13:f.x=h.(x,fIx)&fIx in PFuncs(cRS,bX) by A9,WELLFND1:def 5,PARTFUN1:119;
       per cases;
         suppose 
       A14: for q be Element of X() st q in union(rng fIx) holds P[x,q];then 
       A15: f.x=union(rng fIx)\/{x} by A8,A13;
           hence f.x c= IRS-Seg x\/{x} by A12,XBOOLE_1:9;
           thus x in f.x implies for r be Element of X() st 
             r in union(rng (f|IRS-Seg x)) holds P[x,r] by A14;      
           assume A16:not x in f.x;
           x in {x} by TARSKI:def 1;
           hence thesis by A15,A16,XBOOLE_0:def 2;end;
         suppose 
       A14: ex q be Element of X() st q in union (rng fIx) & not P[x,q];then    
       A15: f.x c= IRS-Seg x & IRS-Seg x c= IRS-Seg x\/{x} 
             by A8,A12,A13,XBOOLE_1:7;
           hence f.x c= IRS-Seg x\/{x} by XBOOLE_1:1;
           thus thesis by A14,A15,WELLORD1:def 1;end;
     end;
A11:for x being Element of RS holds S[x] from WELLFND1:sch 3(A10,A6);
  thus for x,y be Element of X() st x in A & y in A & x <> y holds P[x,y]
    proof  
    A12:now let x be Element of X() such that A13:x in A;
         consider y such that
      A14: x in y & y in rng f by A13,TARSKI:def 4;
         consider z be set such that
      A15: z in dom f & f.z=y by A14,FUNCT_1:def 5;
         reconsider z as Element of RS by A15;
         defpred T[set] means x in f.$1;
      A16: T[z] by A14,A15;
         consider p being Element of RS such that 
      A17: T[p] and 
      A18: not ex q being Element of RS st 
             p <> q & T[q] & [q,p] in IRS from WELLFND1:sch 2(A16,A6);
         p = x
           proof
             assume 
           A19: p<>x;
             set fIp=f|IRS-Seg p;
           A20:f.p=h.(p,fIp) & fIp in PFuncs(cRS, bX) 
               by A9,WELLFND1:def 5,PARTFUN1:119;
             now per cases;
                suppose for q be Element of X() st q in union(rng fIp) 
                                                 holds P[p,q];
                  then f.p=union(rng fIp)\/{p} & not x in {p} 
                    by A8,A19,A20,TARSKI:def 1;
                  hence x in union(rng fIp) by A17,XBOOLE_0:def 2;end;
               suppose ex q be Element of X() st 
                                      q in union (rng fIp) & not P[p,q];
                 hence x in union(rng fIp) by A8,A17,A20;end;end;
             then consider y' be set such that
           A21: x in y' & y' in rng fIp by TARSKI:def 4;
             consider z' be set such that
          A22: z' in dom fIp & fIp.z'=y' by A21,FUNCT_1:def 5;
             reconsider z' as Point of RS by A22;
             z' in IRS-Seg p & f.z'=y' by A22,RELAT_1:86,FUNCT_1:70;
             then z'<> p & [z',p] in IRS & T[z'] by A21,WELLORD1:def 1;
             hence thesis by A18;
           end;
         hence x in f.x by A17;
      end;      
  A13:now let x,y be Element of X() such that 
      A14: x in A & y in A & x <> y & [x,y] in IRS;
          set fIy=f|IRS-Seg y;
          dom f = cRS & x in IRS-Seg y by A14,FUNCT_2:def 1,WELLORD1:def 1;
          then x in dom fIy by RELAT_1:86;
          then x in f.x & fIy.x in rng fIy & fIy.x=f.x 
            by FUNCT_1:def 5,70,A12,A14;
          then y in f.y & x in union(rng fIy) by A12,A14,TARSKI:def 4;
          then P[y,x] by A11;
          hence P[x,y] by A1;
      end;
      let x,y be Element of X() such that 
        A14:x in A & y in A & x <> y;
      R2 well_orders X() by A3,PCOMPS_2:5; 
      then R2 is_connected_in X() by WELLORD1:def 5;
      then [x,y] in IRS or [y,x] in IRS by A14,RELAT_2:def 6;
      then P[x,y] or P[y,x] by A13,A14;
      hence thesis by A1;
    end;
  let x be Element of X();
  per cases;
    suppose 
  A12: x in A;
      take y=x;
      thus thesis by A2,A12;end;
    suppose 
  A12: not x in A;
      not x in f.x
        proof
          assume 
        A13: x in f.x;
          dom f=cRS by FUNCT_2:def 1;
          then f.x in rng f by FUNCT_1:def 5;
          hence thesis by A12,A13,TARSKI:def 4;
        end;
      then consider r be Element of X() such that 
   A13: r in union(rng (f|IRS-Seg x)) & not P[x,r] by A11;
      take r;
      rng (f|IRS-Seg x) c= rng f by RELAT_1:99;
      then union rng (f|IRS-Seg x) c= A by ZFMISC_1:95;
      hence thesis by A13;end;
end;

theorem Th31:
  for M be Reflexive symmetric non empty MetrStruct 
    for r be Real st r > 0 
      ex A be Subset of M st
        (for p,q be Point of M st p <> q & p in A & q in A holds 
           dist(p,q) >= r) &
        for p be Point of M ex q be Point of M st q in A & p in Ball(q,r)
proof
  let M be Reflexive symmetric non empty MetrStruct;
  let r be Real such that 
A1: r > 0;
  defpred P[set,set] means
    for p,q be Point of M st p=$1 & q=$2 holds dist(p,q)>=r;
  set cM=the carrier of M;
A2: for x,y be Element of cM holds P[x,y] iff P[y,x];
A3: for x be Element of cM holds not P[x,x]
  proof
    let x be Element of cM;
    dist(x,x)=0 by METRIC_1:1;
    hence thesis by A1;
  end;
  consider A be Subset of cM such that
A4: for x,y be Element of cM st x in A & y in A & x <> y holds P[x,y] and
A5: for x be Element of cM ex y be Element of cM st y in A & not P[x,y]
     from Th39(A2,A3);
  take A;
  thus for p,q be Point of M st p <> q & p in A & q in A holds 
           dist(p,q) >= r by A4;
  let p be Point of M;
  consider y be Element of cM such that 
A6: y in A & not P[p,y] by A5;
  take y;
  thus thesis by A6,METRIC_1:12;
end;

theorem Th32:
  for M be Reflexive symmetric triangle non empty MetrStruct holds
    M is totally_bounded iff 
        for r be Real,A be Subset of M st r>0 &
             for p,q be Point of M st p <> q & p in A & q in A holds 
                dist(p,q) >= r
           holds A is finite
proof
  let M be Reflexive symmetric triangle non empty MetrStruct;
  thus M is totally_bounded implies
    for r be Real,A be Subset of M st r>0 &
      for p,q be Point of M st p <> q & p in A & q in A holds dist(p,q) >= r
        holds A is finite
  proof
    assume 
  A1:M is totally_bounded;
    let r be Real,A be Subset of M such that 
  A2: r>0 and
  A3:for p,q be Point of M st p <> q & p in A & q in A holds dist(p,q)>=r;
    r/2>0 by A2,XREAL_1:217;
    then consider G be Subset-Family of M such that
  A4: G is finite and 
  A5: the carrier of M = union G and
  A6: for C be Subset of M st C in G ex w be Point of M st C = Ball(w,r/2) 
        by A1,TBSP_1:def 1;
    defpred f[set,set] means $1 in $2 & $2 in G;
  A7:for x st x in A ex y st y in bool(the carrier of M) & f[x,y]
      proof
        let x such that 
      A8: x in A;
        consider y such that
      A9: x in y & y in G by A5,A8,TARSKI:def 4;
        reconsider y as Subset of M by A9;
        take y;
        thus thesis by A9;
      end;
    consider F be Function of A,bool(the carrier of M) such that 
  A8: for x st x in A holds f[x,F.x] from FUNCT_2:sch 1(A7);
    now let x1,x2 be set such that 
    A9: x1 in A & x2 in A & F.x1 = F.x2;
       reconsider p1=x1,p2=x2 as Point of M by A9;
       F.x1 in G by A8,A9;
       then consider w be Point of M such that 
    A10: F.x1 = Ball(w,r/2) by A6;
       p1 in Ball(w,r/2) & p2 in Ball(w,r/2) by A8,A9,A10;
       then dist(p1,w)<r/2 & dist(w,p2)<r/2&dist(p1,p2)<=dist(p1,w)+dist(w,p2) 
         by METRIC_1:4,12;
       then dist(p1,p2)<=dist(p1,w)+dist(w,p2) & dist(p1,w)+dist(w,p2)<r/2+r/2
         by XREAL_1:10;
       then dist(p1,p2)<r/2+r/2 by XXREAL_0:2;
       hence x1 = x2 by A3,A9;
    end;
    then F is one-to-one & dom F=A by FUNCT_2:def 1,25;then 
  A9: A,rng F are_equipotent by WELLORD2:def 4;
    rng F c= G
      proof
        let x such that 
      A10: x in rng F;
        ex y st y in dom F & x=F.y by A10,FUNCT_1:def 5;
        hence thesis by A8;
      end;
    then rng F is finite by A4,FINSET_1:13;
    hence A is finite by A9,CARD_1:68;
  end;
  assume 
A1:for r be Real,A be Subset of M st r>0 &
       for p,q be Point of M st p <> q & p in A & q in A holds dist(p,q) >= r
     holds A is finite;
  let r such that 
A2: r>0;
  consider A be Subset of M such that
A3: for p,q be Point of M st p <> q & p in A & q in A holds dist(p,q) >= r and
A4: for p be Point of M ex q be Point of M st q in A& p in Ball(q,r) 
    by A2,Th31;
A5: A is finite by A1,A2,A3;
  deffunc B(Point of M)=Ball($1,r);
  set BA={B(p) where p is Point of M:p in A};
A6:BA is finite from FRAENKEL:sch 21(A5);   
  BA c= bool the carrier of M
    proof
      let x such that 
    A7: x in BA;
      ex p be Point of M st x = B(p) & p in A  by A7;
      hence thesis;
   end;
 then reconsider BA as Subset-Family of M;
 take BA;
 union BA = the carrier of M
   proof
     the carrier of M c= union BA
       proof
         let x such that 
       A7: x in the carrier of M;
         reconsider p=x as Point of M by A7;
         consider q be Point of M such that 
       A8: q in A & p in B(q) by A4;
         B(q) in BA by A8;
         hence thesis by A8,TARSKI:def 4;
       end;
     hence thesis by XBOOLE_0:def 10;
   end;
   hence BA is finite & union BA = the carrier of M by A6;
   let C be Subset of M such that 
 A7: C in BA;
   ex p be Point of M st C=B(p) & p in A by A7;
   hence thesis;
end;

LocallyFinite:
  for M be Reflexive symmetric triangle non empty MetrStruct
    for  r be Real, A be Subset of M st
         r>0 & for p,q be Point of M st p <> q & p in A & q in A 
           holds dist(p,q) >= r
   for F be Subset-Family of TopSpaceMetr M st 
       F={{x} where x is Element of TopSpaceMetr M: x in A}
     holds F is locally_finite
proof 
  let M be Reflexive symmetric triangle non empty MetrStruct;
  set T=TopSpaceMetr M;
  let r be Real, A be Subset of M such that
A1: r>0 and 
A2: for p,q be Point of M st p <> q & p in A & q in A holds dist(p,q) >= r;
  let F be Subset-Family of T such that
A3: F={{x} where x is Element of T: x in A};
  let x be Point of T;
  reconsider x'=x as Point of M;
  reconsider B=Ball(x',r/2) as Subset of T;
  take B;
  B in Family_open_set M & dist(x',x')=0 & r/2>0
    by A1,PCOMPS_1:33,METRIC_1:1,XREAL_1:217;
  hence x in B & B is open by PRE_TOPC:def 5,METRIC_1:12;  
  set VV={ V where V is Subset of T: V in F & V meets B};
  per cases;
    suppose A6:for p be Point of M st p in A holds dist(p,x') >= r/2;
      VV is empty
        proof
          assume VV is non empty;
          then consider v be set such that 
        A7: v in VV by XBOOLE_0:def 1;
          consider V be Subset of T such that 
        A8: v=V & V in F & V meets B by A7;
          consider y be Point of T such that
        A9: V = {y} & y in A by A3,A8;
          reconsider y as Point of M;
          y in B by A8,A9,ZFMISC_1:56;
          then dist(x',y)<r/2 by METRIC_1:12;
          hence thesis by A6,A9;
        end;
      hence VV is finite;end;
    suppose ex p be Point of M st p in A & dist(p,x') < r/2;
      then consider p be Point of M such that 
    A6: p in A & dist(p,x') < r/2;
      VV c= {{p}}
        proof
          let v be set such that 
        A7: v in VV;
          consider V be Subset of T such that 
        A8: v=V & V in F & V meets B by A7;
          consider y be Point of T such that
        A9: V = {y} & y in A by A3,A8;
          reconsider y as Point of M ;
          y in B by A8,A9,ZFMISC_1:56;
          then dist(x',y)<r/2 by METRIC_1:12;
          then dist(p,y)<=dist(p,x')+dist(x',y) & 
            dist(p,x')+dist(x',y)<r/2+r/2 by A6,METRIC_1:4,XREAL_1:10;
          then dist(p,y)<r/2+r/2 by XXREAL_0:2;
          then p = y & {p} in {{p}} by A2,A6,A9,TARSKI:def 1;
          hence thesis by A8,A9;
        end;
      hence VV is finite by FINSET_1:13;end;
end;

theorem Th33:
  for M be Reflexive symmetric triangle non empty MetrStruct st
      TopSpaceMetr M is countably_compact
    holds M is totally_bounded
proof
  let M be Reflexive symmetric triangle non empty MetrStruct such that
A1: TopSpaceMetr M is countably_compact;
  set T=TopSpaceMetr M;
  assume not M is totally_bounded;
  then consider r be Real, A be Subset of M such that
A2: r>0 and
A3: for p,q be Point of M st p <> q & p in A & q in A holds dist(p,q) >= r and
A4: A is infinite by Th32;
  reconsider A as Subset of T;
  set F={{x} where x is Element of T: x in A};
  reconsider F as Subset-Family of T by RELSET_2:16;
A5:F is locally_finite by A2,A3,LocallyFinite;
  now let a be Subset of T such that 
  A6: a in F;
     ex y be Point of T st a={y} & y in A by A6;
     hence Card a = 1 by CARD_1:50;
  end;then 
A6: F is finite by A1,A5,Th28;
  deffunc P(set)=meet $1;
  set PP={P(y) where y is Subset of T:y in F};
A7: PP is finite from FRAENKEL:sch 21(A6);
  A c= PP
    proof
      let y such that 
    A8: y in A; 
      reconsider y'=y as Point of T by A8;
      {y'} in F & {y'} is Subset of T by A8;
      then P({y'}) in PP;
      hence thesis by SETFAM_1:11;
    end;
  hence thesis by A4,A7,FINSET_1:13;
end;

theorem Th34:
  for M be non empty MetrSpace st M is totally_bounded 
    holds TopSpaceMetr M is second-countable
proof
  let M be non empty MetrSpace such that
A1:M is totally_bounded;
  set T=TopSpaceMetr M;
 defpred F[set,set] means
   for i st i=$1 for G be Subset-Family of T st $2=G holds
     G is finite & the carrier of M = union G &
     for C be Subset of M st C in G ex w be Point of M st C = Ball(w,1/(i+1));
A2: for x st x in NAT ex y st y in bool bool(the carrier of T) & F[x,y]
   proof
     let x such that 
   A3: x in NAT;
     reconsider i=x as Element of NAT by A3;
     1/(i+1)>0 by XREAL_1:141;
     then consider G be Subset-Family of T such that
   A4: G is finite & the carrier of M = union G &
     for C be Subset of M st C in G ex w be Point of M st C=Ball(w,1/(i+1))
       by A1,TBSP_1:def 1;
     take G;
     thus thesis by A4;
   end;
 consider f be Function of NAT,bool bool(the carrier of T) such that
A3: for x st x in NAT holds F[x,f.x] from FUNCT_2:sch 1(A2);
A4: dom f=NAT by FUNCT_2:def 1;
  set U = Union f;
A5:U c= the topology of T
    proof
      let x such that 
    A6: x in U;
      x in union rng f by A6,CARD_3:def 4;
      then consider y such that
    A7: x in y & y in rng f by TARSKI:def 4;
      consider z be set such that 
    A8: z in dom f & f.z=y by A7,FUNCT_1:def 5;
      reconsider z as Element of NAT by A8;
      reconsider fz=f.z as Subset-Family of T;
      reconsider X=x as Subset of T by A7;
      consider w be Point of M such that 
    A9: X=Ball(w,1/(z+1)) by A3,A7,A8;
      thus thesis by A9,PCOMPS_1:33;
    end;
  for A be Subset of T st A is open
    for p be Point of T st p in A
      ex a be Subset of T st a in U & p in a & a c= A
    proof
      let A be Subset of T such that 
    A6: A is open;
      let p be Point of T such that 
    A7: p in A;
      reconsider p'=p as Point of M;
      consider r be real number such that 
    A8: r>0 & Ball(p',r) c= A by A6,A7,TOPMETR:22;
      reconsider r as Real by XREAL_0:def 1;
      r/2 >0 by A8,XREAL_1:217;
      then consider n be Element of NAT such that
    A9: n>0 & 1/n<r/2 by UNIFORM1:2;
      reconsider n1=n-1 as Element of NAT by A9,NAT_1:20;
    A10:f.n1 in rng f by A4,FUNCT_1:def 5;
      reconsider fn=f.n1 as Subset-Family of T;
      the carrier of M = union fn by A3;
      then consider x be set such that
    A11: p in x & x in fn by TARSKI:def 4;
      reconsider x as Subset of M by A11;
      consider w be Point of M such that 
    A12: x=Ball(w,1/(n1+1)) by A3,A11;
      reconsider B=Ball(w,1/n) as Subset of T;
      take B;
      B in union rng f by A10,A11,A12,TARSKI:def 4;
      hence B in U & p in B by A11,A12,CARD_3:def 4;
      let q be set such that 
    A13: q in B;
      reconsider q'=q as Point of M by A13;
      dist(q',w)<1/n & dist(w,p')<1/(n1+1) by A11,A12,A13,METRIC_1:12;
      then dist(q',p')<=dist(q',w)+dist(w,p') & dist(q',w)+dist(w,p')<1/n+1/n
        by METRIC_1:4,XREAL_1:10;
      then dist(q',p')<1/n+1/n & 1/n+1/n<r/2+r/2 by A9,XXREAL_0:2,XREAL_1:10;
      then dist(q',p')<r/2+r/2 by XXREAL_0:2;
      then q in Ball(p',r) by METRIC_1:12;
      hence thesis by A8;
    end;then 
A6: U is Basis of T by A5,YELLOW_9:32;
  now let x such that 
  A7: x in dom f;
     reconsider i=x as Element of NAT by A7;
     reconsider fx=f.i as Subset-Family of T;
     fx is finite by A3;
     hence f.x is countable by CARD_4:43;
  end;
  then U is countable by A4,CARD_4:61,44;then 
A7: Card U c= omega by CARD_4:def 1,CARD_1:83;
  set CB={Card B where B is Basis of T : not contradiction};
  Card U in CB & weight T = meet CB by A6,WAYBEL23:def 5;
  then weight T c= Card U by SETFAM_1:4;
  then weight T c= omega by A7,XBOOLE_1:1;
  hence thesis by WAYBEL23:def 6;
end;

theorem Th35:
  for T be non empty TopSpace holds
    T is second-countable implies
        for F being Subset-Family of T st F is_a_cover_of T & F is open
          ex G being Subset-Family of T
            st G c= F & G is_a_cover_of T & G is countable
proof
  let T be non empty TopSpace;
  assume 
A1: T is second-countable;
  let F being Subset-Family of T such that 
A2: F is_a_cover_of T and 
A3: F is open;
  consider B being Basis of T such that 
A4: B is countable by A1,TOPGEN_4:60;
  defpred P[set,set] means
    for b be Subset of T st b=$1 holds
      ((ex y st y in F & b c= y) implies ($2 in F & b c= $2)) &
       ((for y st y in F holds not b c= y) implies $2={});
A5:for x st x in B ex y st y in bool(the carrier of T) & P[x,y]
    proof
      let x such that 
    A6: x in B;
      reconsider b=x as Subset of T by A6;
      per cases;
        suppose ex y st y in F & b c= y;
          then consider y such that
        A7: y in F & b c= y;
          reconsider y as Subset of T by A7;
          take Y=y;
          thus thesis by A7;end;
        suppose 
        A7: for y st y in F holds not b c= y;
          take E={}T;
          thus thesis by A7;end;
    end;
  consider p be Function of B,bool(the carrier of T) such that
A6: for x st x in B holds P[x,p.x] from FUNCT_2:sch 1(A5);
  take RNG=rng p\{{}};
A7: dom p=B by FUNCT_2:def 1;
  thus RNG c= F
    proof
      let y such that 
    A8: y in RNG;
      y in rng p by A8,XBOOLE_0:def 4;
      then consider z be set such that
    A9: z in dom p & p.z=y by FUNCT_1:def 5;
      reconsider z as Subset of T by A7,A9;
      (ex y st y in F & z c= y) or (for y st y in F holds not z c= y);
      then (p.z in F & z c= p.z or p.z={}) & y<>{} by A8,A6,A9,ZFMISC_1:64;
      hence thesis by A9;
    end;
  thus RNG is_a_cover_of T
    proof
      the carrier of T c= union RNG
        proof
          let y such that 
        A8: y in the carrier of T;
          reconsider q=y as Point of T by A8;
          consider W be Subset of T such that
        A9: q in W & W in F by A2,PCOMPS_1:5;
          W is open by A3,A9,TOPS_2:def 1;
          then consider U be Subset of T such that
        A10: U in B & q in U & U c= W by A9,YELLOW_9:31;
        A11:p.U in rng p by A7,A10,FUNCT_1:def 5;
          then reconsider pU=p.U as Subset of T;
        A12: pU in F & U c= pU by A6,A9,A10;
          then pU in RNG by A10,A11,ZFMISC_1:64;
          hence thesis by A10,A12,TARSKI:def 4;
        end;
      then [#]T=union RNG by XBOOLE_0:def 10;
      hence thesis by PRE_TOPC:def 8;
    end;
  Card rng p c= Card B & Card B c= omega 
    by CARD_4:def 1,CARD_1:83,A4,A7,CARD_2:80;
  then Card rng p c= alef 0 by XBOOLE_1:1,CARD_1:83;
  then rng p is countable by CARD_4:def 1;
  hence thesis by CARD_4:49;
end;

begin :: The main theorem

theorem Th36:
  for M be non empty MetrSpace holds
     TopSpaceMetr M is compact iff TopSpaceMetr M is countably_compact
proof
  let M be non empty MetrSpace;
  set T=TopSpaceMetr M;
  thus T is compact implies T is countably_compact by Th21;
  assume 
A1: T is countably_compact;
  then M is totally_bounded by Th33;then 
A2: T is second-countable by Th34;
  let F be Subset-Family of T such that 
A3: F is_a_cover_of T & F is open;
  consider G be Subset-Family of T such that
A4: G c= F & G is_a_cover_of T & G is countable by A2,A3,Th35;
  G is open by A3,A4,TOPS_2:18;
  then consider H be Subset-Family of T such that
A5: H c= G & H is_a_cover_of T & H is finite by A1,A4,DEF9;
  H c= F by A4,A5,XBOOLE_1:1;
  hence thesis by A5;
end;

theorem Th37:
  for X be set, F be Subset-Family of X st F is finite 
    for A be Subset of X st A is infinite & A c= union F 
      ex Y be Subset of X st Y in F & Y /\ A is infinite
proof
  let X be set, F be Subset-Family of X such that 
A1: F is finite;
  let A be Subset of X such that 
A2: A is infinite & A c= union F;
  set I=INTERSECTION (F,{A});
  Card [:F,{A}:] =Card F by CARD_2:13;
  then Card I<=` Card F by TOPGEN_4:25;then 
A3: I is finite by A1,CARD_2:68;
  defpred P[set,set] means $1 in $2;
A4:for x st x in A ex y st y in I & P[x,y]
    proof
      let x such that 
    A5: x in A;
      consider y such that
    A6: x in y & y in F by A2,A5,TARSKI:def 4;
      take y/\A;
      A in {A} by TARSKI:def 1;
      hence thesis by A5,A6,SETFAM_1:def 5,XBOOLE_0:def 3;
    end;
  consider p be Function of A,I such that
A5: for x st x in A holds P[x,p.x] from FUNCT_2:sch 1(A4);
  consider x such that 
A6: x in A by A2,XBOOLE_0:def 1;
  consider y such that 
A7: y in I & P[x,y] by A4,A6;
  dom p=A & rng p is finite by A3,A7,FUNCT_2:def 1,FINSET_1:13;
  then consider t be set such that
A8: t in rng p & p"{t} is infinite by A2,Th25;
  consider Y,Z be set such that
A9: Y in F & Z in {A} & t=Y/\Z by A8,SETFAM_1:def 5;
  reconsider Y as Subset of X by A9;
  take Y;
A10: Z = A by A9,TARSKI:def 1;
  p"{t} c= Y/\A
    proof
      let z be set such that 
    A11: z in p"{t};
      z in dom p & p.z in {t} by A11,FUNCT_1:def 13;
      then z in A & p.z=t by TARSKI:def 1;
      hence thesis by A5,A9,A10;
    end;
  hence thesis by A8,A9,FINSET_1:13;
end;

theorem
  for M be non empty MetrSpace holds
     TopSpaceMetr M is compact iff M is totally_bounded & M is complete
proof
  let M be non empty MetrSpace;
  set T=TopSpaceMetr M;
  thus T is compact implies M is totally_bounded & M is complete 
    by TBSP_1:10,12;
  assume that
A1: M is totally_bounded and 
A2: M is complete;
  now let A be Subset of T such that A3:A is infinite;
     consider G be Subset-Family of M such that 
  A4: G is finite and 
  A5: the carrier of M = union G and
  A6: for C be Subset of M st C in G ex w be Point of M st C = Ball(w,1/2)
        by A1,TBSP_1:def 1;
      consider X be Subset of M such that
  A7:  X in G & X /\ A is infinite by A3,A4,A5,Th37;
      defpred Q[set] means for a be Subset of M st 
        a=$1 holds a is bounded & a is infinite & a is closed;
      defpred P[set,set] means for a,b be Subset of M st $1=a & $2=b holds 
        b c= a & diameter b <= (diameter a)/2;
      reconsider XA=X/\A as Subset of M;
  A8: XA is bounded & diameter XA <=1
        proof
          consider w be Point of M such that 
        A9: X = Ball(w,1/2) by A6,A7;
          X is bounded & XA c= X by A9,TBSP_1:19,XBOOLE_1:17;
          then XA is bounded & diameter XA <=diameter X & diameter X<=2*(1/2)
            by A9,TBSP_1:21,31,32;
          hence thesis by XXREAL_0:2;
        end;
      reconsider xa=XA as Subset of T;
      reconsider CXA=Cl xa as Subset of M;
      set cM=the carrier of M;
      xa c= Cl xa by PRE_TOPC:48;then
  A9: CXA in bool cM & Q[CXA] by A7,A8,FINSET_1:13,Th9,Th7;
  A10:for x st x in bool cM & Q[x] ex y st y in bool cM & P[x,y] & Q[y]
        proof
          let x such that 
        A11: x in bool cM & Q[x];
          reconsider X=x as Subset of M by A11;
          reconsider X'=X as Subset of T;
          set d=diameter X;
        A12:X is bounded by A11;
          per cases by A12,TBSP_1:29;
             suppose 
          A13:  d=0;
               take Y=X;
               thus thesis by A11,A13;end;
             suppose d>0;then  
          A14:  d/4>0 by XREAL_1:226;
               then consider F be Subset-Family of M such that 
          A15:   F is finite and 
          A16:   cM = union F and
          A17:   for C be Subset of M st C in F ex w be Point of M st 
                       C = Ball(w,d/4) by A1,TBSP_1:def 1;
               X is infinite by A11;
               then consider Y be Subset of M such that
         A18:    Y in F & Y /\ X is infinite by A15,A16,Th37;
               set YX=Y/\X;
               consider w be Point of M such that 
         A19:    Y = Ball(w,d/4) by A17,A18;
               Y is bounded & YX c= Y by A19,TBSP_1:19,XBOOLE_1:17;then 
         A20:  YX is bounded & diameter YX <=diameter Y & diameter Y<=2*(d/4)
                 by A14,A19,TBSP_1:21,31,32;then
         A21: diameter YX<=d/2 by XXREAL_0:2;
              reconsider yx=YX as Subset of T;
              reconsider CYX=Cl yx as Subset of M;
              take CYX; 
         A22: yx c= Cl yx by PRE_TOPC:48;
              X is closed by A11;
              then X' is closed & yx c= X' by XBOOLE_1:17,Th7;
             hence thesis by A22,TOPS_1:31,A20,A21,A18,FINSET_1:13,Th7,Th9;end;
        end;
      consider f be Function such that 
  A11:  dom f = NAT & rng f c= bool cM and
  A12:  f.0 = CXA and
  A13:  for k be Element of NAT
          holds P[f.k,f.(k+1)] & Q[f.k] from TREES_2:sch 5(A9,A10);
      reconsider f as SetSequence of M by A11,FUNCT_2:4;
  A14:now let x such that 
      A15: x in dom f;
         reconsider i=x as Element of NAT by A15;
         f.i is infinite by A13;
         hence f.x is non empty;
      end;
  A15:now let n;
         n in NAT by ORDINAL1:def 13;
         hence f.n is bounded by A13;
      end;
      now let n;
         n in NAT by ORDINAL1:def 13;
         hence f.n is closed by A13;
      end;
      then reconsider f as non-empty bounded closed SetSequence of M
        by A14,A15,def1,def8,FUNCT_1:def 15;
      for n be Element of NAT holds f.(n+1) c= f.n by A13;then 
  A16:f is descending by KURATO_2:def 5;
      deffunc F(Element of NAT)=1/(1+$1);
      consider seq be Real_Sequence such that 
  A17:for n be Element of NAT holds seq.n=F(n) from SEQ_1:sch 1;
      reconsider NULL=0 as Real;
      set Ns=NULL(#)seq;
      for n be Element of NAT holds seq.n=1/(n+1) by A17;then
  A18: seq is convergent & lim seq=0 by SEQ_4:45;then
  A19: Ns is convergent & lim Ns=NULL*0 by SEQ_2:21,22;
      set df=diameter f;
      defpred N[Element of NAT] means Ns.$1 <= df.$1 & df.$1<=seq.$1;
      CXA is bounded by A8,Th9; 
      then 0<=diameter CXA &  diameter CXA <= 1&seq.0=1/(1+0)&Ns.0=NULL*seq.0
        by A8,A17,Th9,TBSP_1:29,SEQ_1:13;then 
  A20:N[0] by A12,def2;
  A21:for n be Element of NAT st N[n] holds N[n+1]
        proof
          let n be Element of NAT such that 
        A22: N[n];set n1=n+1;
          df.n<=F(n) & diameter (f.n1)<=(diameter (f.n))/2& diameter (f.n)=df.n 
            by A13,A17,A22,def2;
          then (df.n)/2<=F(n)/2 & df.n1<=(df.n)/2 by XREAL_1:74,def2;then 
        A23:df.n1<=F(n)/2 by XXREAL_0:2;
          n1+1<=(n1+1)+n by NAT_1:11;
          then F(n1)>=1/(2*n1) & 1/(2*n1)=F(n)/2 by XREAL_1:120,XCMPLX_1:79;
          then 
        A24:F(n1)>=df.n1 by A23,XXREAL_0:2;
          f.n1 is bounded by def1;
          then 0<= diameter (f.n1) & Ns.n1=NULL*seq.n1 by TBSP_1:29,SEQ_1:13;
          hence thesis by A17,A24,def2;
        end;
  A22:for n be Element of NAT holds N[n] from NAT_1:sch 1(A20,A21);then 
  A23:lim df = 0 & df is convergent by A18,A19,SEQ_2:33,34;
      then meet f is non empty by A2,A16,Th11;
      then consider p be set such that
  A24:  p in meet f by XBOOLE_0:def 1;
      reconsider p as Point of T by A24;
      reconsider p'=p as Point of M;
      now let U be open Subset of T such that 
       A25: p in U;
         consider r be real number such that 
       A26: r>0 & Ball(p',r) c= U by A25,TOPMETR:22;
         r/2 >0 by A26,XREAL_1:217;
         then consider n be Element of NAT such that
       A27:  for m be Element of NAT st n<=m holds abs(df.m-0)<r/2 
               by A23,SEQ_2:def 7;
         f.n is infinite by A13;
         then Card {p} <` Card (f.n) & p in f.n by A24,KURATO_2:6,CARD_FIL:1;
         then {p} <>f.n & {p} c= f.n by ZFMISC_1:37;
         then {p} c<f.n by XBOOLE_0:def 8;
         then f.n\{p} <>{} by XBOOLE_1:105;
         then consider q be set such that 
      A28: q in f.n\{p} by XBOOLE_0:def 1;
         reconsider q as Point of T by A28;
         reconsider q'=q as Point of M;
         reconsider B=Ball(q',dist(p',q')) as Subset of T;
         q<>p by A28,ZFMISC_1:64;
         then Ball(q',dist(p',q')) in Family_open_set M & dist(q',q')=0 & 
           dist(p',q')<>0 & dist(p',q')>=0 by PCOMPS_1:33,METRIC_1:1,2,5;
         then B is open & q in B & f.n c= Cl xa & q in f.n
           by A12,A16,A28,KURATO_2:22,ZFMISC_1:64,PRE_TOPC:def 5,METRIC_1:12;
         then B meets xa by PRE_TOPC:54; 
         then consider s be set such that
      A29: s in B & s in xa by XBOOLE_0:3;
         reconsider s as Point of M by A29;
         reconsider s'=s as Point of T;
         take s';
         df.n>=Ns.n & Ns.n=NULL*seq.n & abs(df.n-0)<r/2 by A22,A27,SEQ_1:13;
         then df.n<r/2 & p in f.n & q in f.n & f.n is bounded
           by A13,A24,A28,KURATO_2:6,ZFMISC_1:64,ABSVALUE:def 1;
         then dist(p',q')<=diameter (f.n) & diameter (f.n) < r/2 
           by TBSP_1:def 10,def2;then 
      A30:dist(p',q')<r/2&dist(q',s)<dist(p',q') by A29,METRIC_1:12,XXREAL_0:2;
         then dist(q',s)<r/2 by XXREAL_0:2;
         then dist(p',s)<=dist(p',q')+dist(q',s) & dist(p',q')+dist(q',s)<
           r/2+r/2 by A30,XREAL_1:10,METRIC_1:4;
         then dist(p',s)<r by XXREAL_0:2;
         then s in Ball(p',r) by METRIC_1:12;
         then s in U & s in A by A26,A29,XBOOLE_0:def 3;
         hence s' in A/\U & s'<>p by XBOOLE_0:def 3,A29,METRIC_1:12;
       end;
     hence Der A is non empty by TOPGEN_1:19;
  end;
  then T is countably_compact by Th29;
  hence thesis by Th36;
end;

begin :: Well spaces

definition let T be set;
           let S be Function of NAT,T;
           let i be natural number;
 redefine func S.i -> Element of T;
  coherence
  proof
    reconsider i'=i as Element of NAT by ORDINAL1:def 13;
    S.i'=S.i;
    hence thesis;
  end;
end;

theorem Th39:
  for M be MetrStruct, a be Point of M,x holds
    x in [:X,(the carrier of M)\{a}:]\/{[X,a]} iff
       ex y be set,b be Point of M st
          x=[y,b] & (y in X & b<>a or y = X & b = a)
proof
  let M be MetrStruct,a be Point of M, x;
  thus x in [:X,(the carrier of M)\{a}:]\/{[X,a]} implies
    ex y be set,b be Point of M st
      x=[y,b] & (y in X & b<>a or y = X & b = a)
    proof
      assume 
    A1: x in [:X,(the carrier of M)\{a}:]\/{[X,a]};
      per cases by A1,XBOOLE_0:def 2;
        suppose x in [:X,(the carrier of M)\{a}:];
          then consider x1,x2 be set such that
        A2: x1 in X & x2 in (the carrier of M)\{a} & x=[x1,x2] 
            by ZFMISC_1:def 2;
          reconsider x2 as Point of M by A2;
          take x1,x2;
          thus thesis by A2,ZFMISC_1:64;end;
        suppose x in {[X,a]};
          then x=[X,a] by TARSKI:def 1;
          hence thesis;end;
    end;
  given y be set,b be Point of M such that
A1: x=[y,b] & (y in X & b<>a or y = X & b = a);
  per cases by A1;
    suppose 
  A2: y in X & b<>a;
      the carrier of M is non empty
        proof
          assume the carrier of M is empty;
          then a={} & b={} by SUBSET_1:def 2;
          hence thesis by A2;
        end;
      then b in (the carrier of M)\{a} by A2,ZFMISC_1:64;
      then x in [:X,(the carrier of M)\{a}:] by A1,A2,ZFMISC_1:106;
      hence thesis by XBOOLE_0:def 2;end;
    suppose y = X & b = a;
      then x in {[X,a]} by A1,TARSKI:def 1;
      hence thesis by XBOOLE_0:def 2;end;
end;

definition
  let M be MetrStruct;
  let a be Point of M;
  let X be set;
  func well_dist(a,X) -> Function of
         [:[:X,(the carrier of M)\{a}:]\/{[X,a]},
           [:X,(the carrier of M)\{a}:]\/{[X,a]}:],REAL means :def10:
    for x,y be Element of [:X,(the carrier of M)\{a}:]\/{[X,a]} 
      for x1,y1 be set,x2,y2 be Point of M st x = [x1,x2] & y = [y1,y2] holds
      (x1 = y1 implies it.(x,y) = dist(x2,y2) ) &
      (x1 <> y1 implies it.(x,y) = dist(x2,a)+dist(a,y2) );
  existence
    proof
      set XX=[:X,(the carrier of M)\{a}:]\/{[X,a]};
      defpred P[set,set,set] means
       for x,y be Element of XX st x=$1 & y=$2 
         for x1,y1 be set, x2,y2 be Point of M st x=[x1,x2] & y=[y1,y2] holds           
      (x1=y1 implies $3=dist(x2,y2))&(x1<>y1 implies $3=dist(x2,a)+dist(a,y2));
A1:   for x,y st x in XX & y in XX ex z be set st z in REAL & P[x,y,z]
        proof
          let x,y such that 
        A2: x in XX & y in XX;
          consider x1 be set,x2 be Point of M such that
        A3: x=[x1,x2] & (x1 in X & x2<>a or x1 = X & x2 = a)
            by A2,Th39;
          consider y1 be set,y2 be Point of M such that
        A4: y=[y1,y2] & (y1 in X & y2<>a or y1 = X & y2 = a)
            by A2,Th39;
          now per cases;
             suppose 
             A5: x1 = y1;
               take d=dist(x2,y2);               
               thus d in REAL by XREAL_0:def 1;
               let x',y' be Element of XX such that 
             A6: x' = x & y' = y; 
               let x1',y1' be set, x2',y2' be Point of M such that 
             A7: x' = [x1',x2'] & y' = [y1',y2'];
               x1'=x1 & x2'=x2 & y1'=y1 & y2'=y2 by A3,A4,A6,A7,ZFMISC_1:33;
               hence(x1' = y1' implies d = dist(x2',y2') ) &
                 (x1' <> y1' implies d = dist(x2',a)+dist(a,y2')) by A5;end;
             suppose 
             A5: x1<>y1;
               take d=dist(x2,a)+dist(a,y2);
               thus d in REAL by XREAL_0:def 1;
               let x',y' be Element of XX such that 
             A6: x'=x & y'=y; 
               let x1',y1' be set, x2',y2' be Point of M such that 
             A7: x' = [x1',x2'] & y' = [y1',y2'];
               x1'=x1 & x2'=x2 & y1'=y1 & y2'=y2 by A3,A4,A6,A7,ZFMISC_1:33;
               hence  (x1' = y1' implies d = dist(x2',y2') ) &
                 (x1' <> y1' implies d = dist(x2',a)+dist(a,y2')) by A5;end;
          end;
        hence thesis;
      end;
    consider f being Function of [:XX,XX:],REAL such that
A2:   for x,y st x in XX & y in XX holds P[x,y,f.(x,y)] from BINOP_1:sch 1(A1);
    take f;   
    thus thesis by A2;     
  end;
  uniqueness
  proof
    set XX=[:X,(the carrier of M)\{a}:]\/{[X,a]};
    let w1,w2 be Function of [:XX,XX:],REAL such that
 A1: for x,y be Element of XX
      for x1,y1 be set, x2,y2 be Point of M st x = [x1,x2] & y = [y1,y2] holds
      (x1 = y1 implies w1.(x,y) = dist(x2,y2) ) &
      (x1 <> y1 implies w1.(x,y) = dist(x2,a)+dist(a,y2) ) and
 A2: for x,y be Element of XX
      for x1,y1 be set, x2,y2 be Point of M st x = [x1,x2] & y = [y1,y2] holds
      (x1 = y1 implies w2.(x,y) = dist(x2,y2) ) &
      (x1 <> y1 implies w2.(x,y) = dist(x2,a)+dist(a,y2) );
    now let x,y such that 
    A3: x in XX & y in XX;
          consider x1 be set,x2 be Point of M such that
        A4: x=[x1,x2] & (x1 in X & x2<>a or x1 = X & x2 = a)
            by A3,Th39;
          consider y1 be set,y2 be Point of M such that
        A5: y=[y1,y2] & (y1 in X & y2<>a or y1 = X & y2 = a)
            by A3,Th39;
       reconsider x2,y2 as Point of M;
       x1=y1 or x1<>y1;
       then (w1.(x,y)=dist(x2,y2) & w2.(x,y)=dist(x2,y2)) or 
            (w1.(x,y)=dist(x2,a)+dist(a,y2) & w2.(x,y)=dist(x2,a)+dist(a,y2))
         by A1,A2,A3,A4,A5;
       hence w1.(x,y)=w2.(x,y);
    end;
    hence thesis by BINOP_1:1;
  end;
end;

theorem
  for M be MetrStruct,a be Point of M
      for X be non empty set holds
    ( well_dist(a,X) is Reflexive           implies M is Reflexive  ) &
    ( well_dist(a,X) is symmetric           implies M is symmetric  ) &
    ( well_dist(a,X) is triangle Reflexive  implies M is triangle   ) &
    (well_dist(a,X) is discerning Reflexive implies M is discerning )
proof
  let M be MetrStruct,A be Point of M;
  let X be non empty set;
  consider x0 be set such that
A0: x0 in X by XBOOLE_0:def 1;
  set XX=[:X,(the carrier of M)\{A}:]\/{[X,A]};
  set w=well_dist(A,X);thus 
W1:w is Reflexive implies  M is Reflexive
    proof
      assume 
    A3: w is Reflexive;
      now let a be Element of M;
        now per cases;
          suppose a=A; then 
          A4: [X,a] in XX by Th39;
            hence dist(a,a) = w.([X,a],[X,a]) by def10
                           .= 0 by A3,A4,METRIC_1:def 3;end;
          suppose a<>A; then 
          A4: [x0,a] in XX by A0,Th39;
            hence dist(a,a) = w.([x0,a],[x0,a]) by def10
                           .= 0 by A3,A4,METRIC_1:def 3;end;
        end;
        hence dist(a,a) = 0;  
      end;
      hence thesis by METRIC_1:1;
    end;
  thus w is symmetric implies M is symmetric
    proof
      assume 
    A3:w is symmetric;
      now let a,b be Element of M;
        now per cases;
          suppose a=A & b=A;
            hence dist(a,b)=dist(b,a);end;
          suppose 
          A4: a=A & b<>A;then 
          A5: [X,A] in XX & [x0,b] in XX by A0,Th39;
          A6: X<>x0 by A0;
            then dist(A,A)+dist(A,b) = w.([X,A],[x0,b]) by A5,def10
                                    .= w.([x0,b],[X,A]) by A3,A5,METRIC_1:def 5
                                    .= dist(b,A)+dist(A,A) by A5,A6,def10;
            hence dist(a,b)=dist(b,a) by A4;end;
          suppose 
          A4: a<>A & b=A;then 
          A5: [X,A] in XX & [x0,a] in XX by A0,Th39;
          A6: X<>x0 by A0;
            then dist(A,A)+dist(A,a) = w.([X,A],[x0,a]) by A5,def10
                                    .= w.([x0,a],[X,A]) by A3,A5,METRIC_1:def 5
                                    .= dist(a,A)+dist(A,A) by A5,A6,def10;
            hence dist(a,b)=dist(b,a) by A4;end;
          suppose a<>A & b<>A;then 
          A5: [x0,a] in XX & [x0,b] in XX by A0,Th39;
             hence dist(a,b) = w.([x0,a],[x0,b]) by def10
                            .= w.([x0,b],[x0,a]) by A3,A5,METRIC_1:def 5
                            .= dist(b,a) by A5,def10;end;
        end;
        hence dist(a,b) = dist(b,a);
      end;
      hence thesis by METRIC_1:3;
    end;    
  thus w is triangle Reflexive implies M is triangle
    proof
      assume 
    A3: w is triangle Reflexive;
      now let a,b,c be Point of M;
         now per cases;
           suppose a=A & b=A & c =A;
             then reconsider Xa=[X,a],Xb=[X,b],Xc =[X,c] as Element of XX 
               by Th39;
             w.(Xa,Xc)<=w.(Xa,Xb)+w.(Xb,Xc) & dist(a,c)=w.(Xa,Xc) &
               dist(a,b)=w.(Xa,Xb) & dist(b,c)=w.(Xb,Xc)
               by A3,def10,METRIC_1:def 6;
             hence dist(a,c)<=dist(a,b)+dist(b,c);end;
           suppose 
           A4: a=A & b=A & c <> A;
             then reconsider Xa=[X,a],Xb=[X,b],Xc =[x0,c] as Element of XX 
               by A0,Th39;
             x0<>X by A0;
             then w.(Xa,Xc)<=w.(Xa,Xb)+w.(Xb,Xc) & dist(a,b)=w.(Xa,Xb) & 
               dist(a,a)+dist(a,c)=w.(Xa,Xc) & dist(a,a)+dist(b,c)=w.(Xb,Xc)& 
               dist(a,a)=0 by A3,W1,A4,def10,METRIC_1:def 6,METRIC_1:1;
             hence dist(a,c)<=dist(a,b)+dist(b,c);end;
           suppose 
           A4: a=A & b<>A & c = A;
             then reconsider Xa=[X,a],Xb=[x0,b],Xc =[X,c] as Element of XX 
               by A0,Th39;
             x0<>X by A0;
             then w.(Xa,Xc)<=w.(Xa,Xb)+w.(Xb,Xc) & dist(a,c)=w.(Xa,Xc) &
               dist(a,a)+dist(a,b)=w.(Xa,Xb) & dist(b,c)+dist(a,a)=w.(Xb,Xc) & 
               dist(a,a)=0 by A3,W1,A4,def10,METRIC_1:1,def 6;
             hence dist(a,c)<=dist(a,b)+dist(b,c);end;
           suppose 
           A4: a=A & b<>A & c <> A;
             then reconsider Xa=[X,a],Xb=[x0,b],Xc =[x0,c] as Element of XX 
               by A0,Th39;
             x0<>X by A0;
             then w.(Xa,Xc)<=w.(Xa,Xb)+w.(Xb,Xc)&dist(a,a)+dist(a,c)=w.(Xa,Xc)&
               dist(a,a)+dist(a,b)=w.(Xa,Xb)&dist(b,c)=w.(Xb,Xc)&dist(a,a)=0
               by A3,W1,A4,def10,METRIC_1:def 6,1;
             hence dist(a,c)<=dist(a,b)+dist(b,c);end;
           suppose 
           A4: a<>A & b=A & c =A;
             then reconsider Xa=[x0,a],Xb=[X,b],Xc =[X,c] as Element of XX 
               by A0,Th39;
             x0<>X by A0;
             then w.(Xa,Xc)<=w.(Xa,Xb)+w.(Xb,Xc)&dist(a,c)+dist(c,c)=w.(Xa,Xc)&
               dist(a,b)+dist(c,c)=w.(Xa,Xb) & dist(b,c)=w.(Xb,Xc)&dist(c,c)=0
               by A3,W1,A4,def10,METRIC_1:1,def 6;
             hence dist(a,c)<=dist(a,b)+dist(b,c);end;
           suppose 
           A4: a<>A & b=A & c <>A; 
             then reconsider Xa=[x0,a],Xb=[X,b],Xc =[x0,c] as Element of XX 
               by A0,Th39;
             x0<>X by A0;
             then w.(Xa,Xc)<=w.(Xa,Xb)+w.(Xb,Xc) & dist(a,c)=w.(Xa,Xc) &
               dist(a,b)+dist(b,b)=w.(Xa,Xb) & dist(b,b)+dist(b,c)=w.(Xb,Xc)& 
               dist(b,b)=0 by W1,A3,A4,def10,METRIC_1:1,def 6;
             hence dist(a,c)<=dist(a,b)+dist(b,c);end;
           suppose A4:a<>A & b<>A & c = A;
             then reconsider Xa=[x0,a],Xb=[x0,b],Xc =[X,c] as Element of XX 
               by A0,Th39;
             x0<>X by A0;
             then w.(Xa,Xc)<=w.(Xa,Xb)+w.(Xb,Xc)&dist(a,c)+dist(c,c)=w.(Xa,Xc)&
               dist(a,b)=w.(Xa,Xb) & dist(b,c)+dist(c,c)=w.(Xb,Xc) & 
               dist(c,c)=0 by A3,W1,A4,def10,METRIC_1:def 6,1;
             hence dist(a,c)<=dist(a,b)+dist(b,c);end;
           suppose a<>A & b<>A & c <> A;
             then reconsider Xa=[x0,a],Xb=[x0,b],Xc =[x0,c] as Element of XX 
               by A0,Th39;
             w.(Xa,Xc)<=w.(Xa,Xb)+w.(Xb,Xc) & dist(a,c)=w.(Xa,Xc) &
               dist(a,b)=w.(Xa,Xb) & dist(b,c)=w.(Xb,Xc)
               by A3,def10,METRIC_1:def 6;
             hence dist(a,c)<=dist(a,b)+dist(b,c);end;
         end;
         hence dist(a,c)<=dist(a,b)+dist(b,c);
      end;
      hence thesis by METRIC_1:4;
    end;
  assume 
A3:w is discerning Reflexive;
  now let a,b be Point of M;
     assume 
  A4: dist(a,b)=0;
     now per cases;
        suppose a=A & b=A;
          hence a=b;end;
        suppose A5:a=A & b<>A;
          then reconsider Xa=[X,a],Xb=[x0,b] as Element of XX by A0,Th39;
          x0<>X by A0;
          then dist(a,a)+dist(a,b)=w.(Xa,Xb) & dist(a,a)=0 
            by A3,W1,A5,def10,METRIC_1:1;
          then Xa=Xb by A3,A4,METRIC_1:def 4;
          hence a=b by ZFMISC_1:33;end;
        suppose A5:a<>A & b=A;
          then reconsider Xa=[x0,a],Xb=[X,b] as Element of XX by A0,Th39;
          x0<>X by A0;
          then dist(a,b)+dist(b,b)=w.(Xa,Xb) & dist(b,b)=0 
            by A3,W1,A5,def10,METRIC_1:1;
          then Xa=Xb by A3,A4,METRIC_1:def 4;
          hence a=b by ZFMISC_1:33;end;
        suppose a<>A & b<>A;
          then reconsider Xa=[x0,a],Xb=[x0,b] as Element of XX by A0,Th39;
          dist(a,b)=w.(Xa,Xb) by def10;
          then Xa=Xb by A3,A4,METRIC_1:def 4;
          hence a=b by ZFMISC_1:33;end;
     end;
     hence a=b;
  end;
  hence thesis by METRIC_1:2;
end;

definition 
  let M be MetrStruct;
  let a be Point of M;
  let X be set;
  func WellSpace(a,X) -> strict MetrStruct equals
    MetrStruct (#[:X,(the carrier of M)\{a}:]\/{[X,a]},well_dist(a,X)#);
  coherence;
end;

registration
  let M be MetrStruct;
  let a be Point of M;
  let X be set;
  cluster WellSpace(a,X) -> non empty;
  coherence;
end;

PPP1:for M be MetrStruct,a be Point of M,X holds
  (M is Reflexive implies WellSpace(a,X) is Reflexive) &
  (M is symmetric implies WellSpace(a,X) is symmetric) &
  (M is triangle symmetric Reflexive implies WellSpace(a,X) is triangle)&
  (M is triangle symmetric Reflexive discerning implies 
    WellSpace(a,X) is discerning)
proof
  let M be MetrStruct,a be Point of M,X;
  set XX=[:X,(the carrier of M)\{a}:]\/{[X,a]};
  set w=well_dist(a,X);
  set W=WellSpace(a,X);
  thus M is Reflexive implies W is Reflexive
    proof
      assume 
    A1: M is Reflexive;      
      now let A be Element of XX;
         consider y be set,b be Point of M such that
       A2: A=[y,b] & (y in X & b<>a or y = X & b = a) by Th39;
         thus w.(A,A) = dist(b,b) by A2,def10
                     .= 0 by A1,METRIC_1:1;
      end;
      then w is Reflexive by METRIC_1:def 3;
      hence thesis by METRIC_1:def 7;
    end;
  thus M is symmetric implies W is symmetric
    proof
      assume 
    A1: M is symmetric;
      now let A,B be Element of XX;
         consider y1 be set,b1 be Point of M such that
      A2: A=[y1,b1] & (y1 in X & b1<>a or y1 = X & b1 = a) by Th39;
         consider y2 be set,b2 be Point of M such that
      A3: B=[y2,b2] & (y2 in X & b2<>a or y2 = X & b2 = a) by Th39;
         now per cases by A2,A3;
            suppose b1=a & y1=X & b2=a & y2=X;
              hence w.(A,B)=w.(B,A) by A2,A3;end;
            suppose 
            A4: y1 <>y2;
              hence w.(A,B) = dist(b1,a)+dist(a,b2) by A2,A3,def10
                           .= dist(a,b1)+dist(a,b2) by A1,METRIC_1:3
                           .= dist(a,b1)+dist(b2,a) by A1,METRIC_1:3
                           .= w.(B,A) by A2,A3,A4,def10;end;
            suppose 
            A4: b1<>a & b2<>a & y1=y2;
              hence w.(A,B) = dist(b1,b2) by A2,A3,def10
                           .= dist(b2,b1) by A1,METRIC_1:3
                           .=w.(B,A) by A2,A3,A4,def10;end;
         end;
         hence w.(A,B)=w.(B,A);
      end;
      then w is symmetric by METRIC_1:def 5;
      hence thesis by METRIC_1:def 9;
    end;
  thus M is triangle symmetric Reflexive implies WellSpace(a,X) is triangle
    proof
      assume 
    A1: M is triangle symmetric Reflexive;
      now let A,B,C be Element of XX;
         consider y1 be set,b1 be Point of M such that
      A2:  A=[y1,b1] & (y1 in X & b1<>a or y1 = X & b1 = a) by Th39;
         consider y2 be set,b2 be Point of M such that
      A3:  B=[y2,b2] & (y2 in X & b2<>a or y2 = X & b2 = a) by Th39;
         consider y3 be set,b3 be Point of M such that
      A4:  C=[y3,b3] & (y3 in X & b3<>a or y3 = X & b3 = a) by Th39;
         now per cases;
            suppose y1=y2 & y1=y3;
              then dist(b1,b3)=w.(A,C)&dist(b1,b2)=w.(A,B)&dist(b2,b3)=w.(B,C)&
                dist(b1,b3)<=dist(b1,b2)+dist(b2,b3) 
                by A1,A2,A3,A4,def10,METRIC_1:4;
              hence w.(A,C)<=w.(A,B)+w.(B,C);end;
            suppose y1<>y2 & y1=y3;then 
            A5: dist(b1,b3)=w.(A,C) & dist(b1,a)+dist(a,b2)=w.(A,B) & 
               dist(b2,a)+dist(a,b3)=w.(B,C)&dist(b1,b2)<=dist(b1,a)+dist(a,b2)
                & dist(b2,b3)<=dist(b2,a)+dist(a,b3)
                by A1,A2,A3,A4,def10,METRIC_1:4;
              then dist(b1,b2)+dist(b2,b3)<=w.(A,B)+w.(B,C) & dist(b1,b3)<=
                dist(b1,b2)+dist(b2,b3) by XREAL_1:9,A1,METRIC_1:4;
              hence w.(A,C)<=w.(A,B)+w.(B,C) by A5,XXREAL_0:2;end;
            suppose y1=y2 & y1<>y3;then 
            A5: dist(b1,a)+dist(a,b3)=w.(A,C) & dist(b1,b2)=w.(A,B) & 
                dist(b2,a)+dist(a,b3)=w.(B,C) & dist(b1,a)<=dist(b1,b2) + 
                dist(b2,a) by A1,A2,A3,A4,def10,METRIC_1:4;
              then w.(A,C)<=dist(b1,b2)+dist(b2,a)+dist(a,b3)by XREAL_1:8;
              hence w.(A,C)<=w.(A,B)+w.(B,C) by A5;end;
            suppose y1<>y2 & y1<>y3 & y2<>y3;then 
            A5: dist(b1,a)+dist(a,b3)=w.(A,C) & dist(b1,a)+dist(a,b2)=w.(A,B) & 
                dist(b2,a)+dist(a,b3)=w.(B,C) by A2,A3,A4,def10;
              0<=dist(a,b2) & 0<=dist(b2,a) by A1,METRIC_1:5;
              then dist(b1,a)+0<=w.(A,B)&0+dist(a,b3)<=w.(B,C) by A5,XREAL_1:8;
              hence w.(A,C)<=w.(A,B)+w.(B,C) by A5,XREAL_1:9;end;
            suppose y1<>y2 & y1<>y3 & y2=y3;then 
            A5: dist(b1,a)+dist(a,b3)=w.(A,C) & dist(b1,a)+dist(a,b2)=w.(A,B)& 
                dist(b2,b3)=w.(B,C) & dist(a,b3)<=dist(a,b2)+dist(b2,b3)
                by A1,A2,A3,A4,def10,METRIC_1:4;
              then w.(A,C)<=dist(b1,a)+(dist(a,b2)+dist(b2,b3)) by XREAL_1:9;
              hence w.(A,C)<=w.(A,B)+w.(B,C) by A5;end;
         end;
         hence w.(A,C)<=w.(A,B)+w.(B,C);
       end;
     then w is triangle by METRIC_1:def 6;
     hence thesis by METRIC_1:def 10;
   end;
  assume 
A1: M is triangle symmetric Reflexive discerning;
  now let A,B be Element of XX;
     assume 
  A2: w.(A,B)=0;
     consider y1 be set,b1 be Point of M such that
  A3:  A=[y1,b1] & (y1 in X & b1<>a or y1 = X & b1 = a) by Th39;
     consider y2 be set,b2 be Point of M such that
  A4:  B=[y2,b2] & (y2 in X & b2<>a or y2 = X & b2 = a) by Th39;
     now per cases;
        suppose 
        A5: y1=y2;
          then w.(A,B)=dist(b1,b2) by A3,A4,def10;
          hence A=B by A1,A2,METRIC_1:2,A3,A4,A5;end;
        suppose y1<>y2;
          then w.(A,B)=dist(b1,a)+dist(a,b2) & dist(a,b2)>=0 & dist(b1,a)>=0
            by A1,A3,A4,def10,METRIC_1:5;
          then dist(b1,a)=0 & dist(a,b2)=0 by A2,XREAL_1:29;
          hence A=B by A1,METRIC_1:2,A3,A4;end;
     end;
     hence A=B;
  end;
  then w is discerning by METRIC_1:def 4;
  hence thesis by METRIC_1:def 8;
end;

registration
  let M be Reflexive MetrStruct;
  let a be Point of M;
  let X be set;
  cluster WellSpace(a,X) -> Reflexive;
  coherence by PPP1;
end;

registration
  let M be symmetric MetrStruct;
  let a be Point of M;
  let X be set;
  cluster WellSpace(a,X) -> symmetric;
  coherence by PPP1;
end;

registration
  let M be symmetric triangle Reflexive MetrStruct;
  let a be Point of M;
  let X be set;
  cluster WellSpace(a,X) -> triangle;
  coherence by PPP1;
end;

registration
  let M be MetrSpace;
  let a be Point of M;
  let X be set;
  cluster WellSpace(a,X) -> discerning;
  coherence by PPP1;
end;

theorem
  for M be triangle Reflexive non empty MetrStruct
    for a be Point of M 
      for X be non empty set holds
      WellSpace(a,X) is complete implies M is complete 
proof
  let M be triangle Reflexive non empty MetrStruct;
  let a be Point of M;
  let X be non empty set;
  consider x0 be set such that
A0: x0 in X by XBOOLE_0:def 1;
  assume 
A1: WellSpace(a,X) is complete;
  set W=WellSpace(a,X);
  set XX=[:X,(the carrier of M)\{a}:]\/{[X,a]};
  let S be sequence of M such that 
A2: S is Cauchy;
  defpred P[set,set] means 
    (S.$1<>a implies $2=[x0,S.$1]) & (S.$1=a implies $2=[X,S.$1]);
A3:for x st x in NAT ex y st y in the carrier of W & P[x,y]
    proof
      let x such that 
    A4: x in NAT;
      reconsider i=x as Element of NAT by A4;
      per cases;
        suppose 
        A5: S.i<>a;
          take xS=[x0,S.i];
          thus thesis by A0,A5,Th39;end;
        suppose 
        A5: S.x=a;
          take xS=[X,a];
          thus thesis by A5,Th39;end;
    end;
  consider S' be sequence of W such that
A4: for x st x in NAT holds P[x,S'.x] from FUNCT_2:sch 1(A3);
  S' is Cauchy
    proof
      let r such that 
    A5: r>0;
      consider p be Element of NAT such that 
    A6: for n,m be Element of NAT st p<=n & p<=m holds dist(S.n,S.m)<r 
          by A2,A5,TBSP_1:def 5;
      take p;
      let n,m be Element of NAT such that 
    A7: p <= n & p <= m;
      per cases;
        suppose S.n=a & S.m=a;
          then [X,S.n]=S'.n & [X,S.m]=S'.m by A4;
          then dist(S'.n,S'.m)=dist(S.n,S.m) by def10;
          hence thesis by A6,A7;end;
        suppose 
        A8: S.n<>a & S.m=a;
          then [x0,S.n]=S'.n & [X,S.m]=S'.m & X<>x0 by A0,A4;
          then dist(S'.n,S'.m)=dist(S.n,S.m)+dist(S.m,S.m) & dist(S.m,S.m)=0
            by A8,def10,METRIC_1:1;
          hence thesis by A6,A7;end;
        suppose 
        A8: S.n=a & S.m<>a;
          then [X,S.n]=S'.n & [x0,S.m]=S'.m & X<>x0 by A0,A4;
          then dist(S'.n,S'.m)=dist(S.n,S.n)+dist(S.n,S.m) & dist(S.n,S.n)=0
            by A8,def10,METRIC_1:1;
          hence thesis by A6,A7;end;
        suppose S.n<>a & S.m<>a;
          then [x0,S.n]=S'.n & [x0,S.m]=S'.m by A4;
          then dist(S'.n,S'.m)=dist(S.n,S.m) by def10;
          hence thesis by A6,A7;end;
    end;
  then S' is convergent by A1,TBSP_1:def 6;
  then consider L being Element of W such that
A6: for r st r>0 ex n be Element of NAT st 
      for m be Element of NAT st n<=m holds dist(S'.m,L)<r by TBSP_1:def 3;
  consider L1 be set,L2 be Point of M such that
A7: L=[L1,L2] & (L1 in X & L2<>a or L1 = X & L2 = a) by Th39;
  take L2;
  let r such that 
A8: r>0;
  consider n be Element of NAT such that
A9: for m be Element of NAT st n<=m holds dist(S'.m,L)<r by A6,A8;
  take n;
  let m be Element of NAT such that 
A10: n<=m;
  per cases;
    suppose 
  A12: S.m=a & L1=X;
      then S'.m=[X,a] by A4;
      then dist(S'.m,L)=dist(S.m,L2) by A7,A12,def10;
      hence thesis by A10,A9;end;
    suppose 
  A12: S.m=a & L1<>X;
      then S'.m=[X,a] by A4;
      then dist(S'.m,L)=dist(S.m,S.m)+dist(S.m,L2) & dist(S.m,S.m)=0
        by A7,A12,def10,METRIC_1:1;
      hence thesis by A10,A9;end;
    suppose 
  A12: S.m <> a & L1=x0;
      then S'.m=[x0,S.m] by A4;
      then dist(S'.m,L)=dist(S.m,L2) by A7,A12,def10;
      hence thesis by A10,A9;end;
    suppose 
  A12: S.m <> a & L1<>x0;
      then S'.m=[x0,S.m] by A4;
      then dist(S'.m,L)=dist(S.m,a)+dist(a,L2) & dist(S.m,a)+dist(a,L2)>=
        dist(S.m,L2) & dist(S'.m,L)<r by A7,A9,A10,A12,def10,METRIC_1:4;
      hence thesis by XXREAL_0:2;end;
end;

theorem Th42:
  for M be symmetric triangle Reflexive non empty MetrStruct
    for a be Point of M 
      for S be sequence of WellSpace(a,X) st S is Cauchy holds
  (for Xa be Point of WellSpace(a,X) st Xa=[X,a]
     for r st r > 0 ex n st for m st m >= n holds dist(S.m,Xa) < r)
     or
   ex n,Y st for m st m >= n ex p be Point of M st S.m = [Y,p]
proof
  let M be symmetric triangle Reflexive non empty MetrStruct;
  let a be Point of M;
  set W=WellSpace(a,X);
  set XX=[:X,(the carrier of M)\{a}:]\/{[X,a]};
  set w=well_dist(a,X);
  let S be sequence of W such that 
A1: S is Cauchy;
  reconsider Xa=[X,a] as Point of W by Th39;
  per cases;
    suppose for r st r > 0 ex n st for m st m >= n holds 
              dist(S.m,Xa) < r;
      hence thesis;end;
    suppose ex r st r > 0 & for n ex m st m >= n & dist(S.m,Xa) >= r;
      then consider r be Real such that
    A3: r > 0 and 
    A4: for n ex m st m >= n & dist(S.m,Xa) >= r;
      consider p be Element of NAT such that
    A5: for n,m be Element of NAT st n>=p & m>=p holds dist(S.n,S.m)<r 
        by A1,A3,TBSP_1:def 5;
      consider p' be natural number such that 
    A6: p' >= p & dist(S.p',Xa) >= r by A4; 
      consider Y be set,y be Point of M such that
    A8:S.p'=[Y,y] & (Y in X & y<>a or Y = X & y = a) by Th39;
      ex n,Y st for m st m >= n ex p be Point of M st S.m = [Y,p]
        proof
          take p',Y;          
          let m such that 
        A9: m >= p';
           consider Z be set,z be Point of M such that
        A10:S.m=[Z,z] & (Z in X & z<>a or Z = X & z = a) by Th39;     
          Y = Z
            proof
              assume 
            A11: Y<>Z;
              (X=Y or X<>Y) & dist(a,a)=0 by METRIC_1:1;
              then dist(S.p',Xa)=dist(y,a) or dist(S.p',Xa)=dist(y,a)+0 
                by A8,def10;
              then dist(y,a)>=r & dist(a,z) >=0 by A6,METRIC_1:5;
              then dist(y,a)+dist(a,z)>=r+0 & m>=p & m in NAT & p' in NAT 
                by A6,A9,XREAL_1:9,XXREAL_0:2,ORDINAL1:def 13;
              then dist(S.p',S.m)>=r &dist(S.p',S.m)<r 
                by A5,A6,A8,A10,A11,def10;
              hence thesis;
            end;
          hence thesis by A10;
        end;
      hence thesis;end;
end;

theorem Th43:
  for M be symmetric triangle Reflexive non empty MetrStruct
    for a be Point of M holds
      M is complete implies WellSpace(a,X) is complete
proof
  let M be symmetric triangle Reflexive non empty MetrStruct;
  let a be Point of M;
  assume 
A1: M is complete;
  set W=WellSpace(a,X);
  set XX=[:X,(the carrier of M)\{a}:]\/{[X,a]};
  let S' be sequence of W such that 
A2: S' is Cauchy;
  defpred P[set,set] means 
    ex x st S'.$1=[x,$2];
A3: for x st x in NAT ex y st y in the carrier of M & P[x,y]
    proof
      let x such that 
    A4: x in NAT;
      reconsider i=x as Element of NAT by A4;
       consider s1 be set,s2 be Point of M such that
    A5: S'.i=[s1,s2] & (s1 in X & s2<>a or s1 = X & s2 = a) by Th39;
      take s2;
      thus thesis by A5;
    end;
  consider S be sequence of M such that
A4: for x st x in NAT holds P[x,S.x] from FUNCT_2:sch 1(A3);
  S is Cauchy
    proof
      let r such that 
    A5: r>0;
      consider p be Element of NAT such that 
    A6: for n,m be Element of NAT st p<=n & p<=m holds dist(S'.n,S'.m)<r 
        by A2,A5,TBSP_1:def 5;
      take p;
      let n,m be Element of NAT such that 
    A7: p<=n & p<=m;
      consider x such that 
    A8:S'.n=[x,S.n] by A4;
      consider y such that 
    A9:S'.m=[y,S.m] by A4;
      per cases;
        suppose x=y;
          then dist(S'.n,S'.m)=dist(S.n,S.m) by A8,A9,def10;
          hence thesis by A6,A7;end;
        suppose x<>y;
          then dist(S'.n,S'.m)=dist(S.n,a)+dist(a,S.m) &
            dist(S.n,S.m) <= dist(S.n,a)+dist(a,S.m) & dist(S'.n,S'.m)<r 
            by A6,A7,A8,A9,def10,METRIC_1:4;
          hence thesis by XXREAL_0:2;end;  
    end;
  then S is convergent by A1,TBSP_1:def 6;
  then consider L being Element of M such that
A6: for r st r>0 ex n be Element of NAT st 
      for m be Element of NAT st n<=m holds dist(S.m,L)<r by TBSP_1:def 3;
  reconsider Xa=[X,a] as Point of W by Th39;
  per cases by A2,Th42;
    suppose B2:L=a;
      take Xa;
      let r such that 
    A7: r > 0;
      consider n be Element of NAT such that
    A8: for m be Element of NAT st n<=m holds dist(S.m,L)<r by A6,A7;
      take n;
      let m be Element of NAT such that 
    A9: m >=n;
      consider x such that 
    A10:  S'.m=[x,S.m] by A4;
      (x=X or x<>X)& dist(a,a)=0 by METRIC_1:1;
      then dist(S'.m,Xa)=dist(S.m,L) or dist(S'.m,Xa)=dist(S.m,L)+0 
        by A10,B2,def10;
      hence dist(S'.m,Xa)<r by A8,A9;end;
    suppose 
    A7: for Xa be Point of W st Xa=[X,a]
        for r st r > 0 ex n st for m st m >= n holds dist(S'.m,Xa) < r;
      take Xa;
      let r such that 
    A8: r > 0;
      consider n such that 
    A9: for m st m >= n holds dist(S'.m,Xa) < r by A7,A8;
      reconsider n as Element of NAT by ORDINAL1:def 13;
      take n;
      let m be Element of NAT such that 
    A10: m >= n;
      thus dist(S'.m,Xa) < r by A9,A10;end;
    suppose 
      A7: a<>L & ex n,Y st for m st m >= n 
          ex p be Point of M st S'.m = [Y,p];
      then consider n,Y such that 
    A9: for m st m >= n ex p be Point of M st S'.m = [Y,p];
      consider s1 be set,s2 be Point of M such that
    D1: S'.n=[s1,s2] & (s1 in X & s2<>a or s1 = X & s2 = a) by Th39;    
      consider s3 be Point of M such that 
    D2:S'.n = [Y,s3] by A9;
      per cases by D1,D2,ZFMISC_1:33;
        suppose Y in X;
          then reconsider YL=[Y,L] as Point of W by A7,Th39;
          take YL;
          let r such that 
        A10: r > 0;
          consider p be Element of NAT such that
        A11: for m be Element of NAT st p<=m holds dist(S.m,L)<r by A6,A10;
          max(p,n)=p or max(p,n)=n by XXREAL_0:16;
          then reconsider mm=max(p,n) as Element of NAT by ORDINAL1:def 13;
          take mm;
          let m be Element of NAT such that 
        A12: m >= mm;
          mm >= n by XXREAL_0:25;
          then m >= n by A12,XXREAL_0:2;
          then consider pm be Point of M such that 
        A13: S'.m = [Y,pm] by A9;
          consider x such that 
        A14:S'.m=[x,S.m] by A4;
          mm >= p by XXREAL_0:25;then 
        A15:m>=p by A12,XXREAL_0:2;
          x=Y by A13,A14,ZFMISC_1:33;
          then dist(S'.m,YL)=dist(S.m,L) by A14,def10;
          hence dist(S'.m,YL)<r by A11,A15;end;
        suppose 
        A10: Y=X;
          take Xa;
          let r such that 
        A11: r > 0;
          reconsider n as Element of NAT by ORDINAL1:def 13; 
          take n;
          let m be Element of NAT such that 
        A12: m >= n;
          consider t1 be set,t2 be Point of M such that
        A13: S'.m=[t1,t2] & (t1 in X & t2<>a or t1 = X & t2 = a) by Th39;
          consider t3 be Point of M such that 
        A14:S'.m = [Y,t3] by A9,A12;
          Y=t1 & t2=t3 by A13,A14,ZFMISC_1:33;
          hence dist(S'.m,Xa)<r by A11,A10,A13,METRIC_1:1;end;end;
end;

theorem Th44:
  for M be symmetric triangle Reflexive non empty MetrStruct st
        M is complete
    for a be Point of M st 
        ex b be Point of M st dist(a,b)<>0
      for X be infinite set holds 
  WellSpace(a,X) is complete & 
  ex S be non-empty bounded SetSequence of WellSpace(a,X) st
     S is closed & S is descending & meet S is empty
proof
  let M be symmetric triangle Reflexive non empty MetrStruct such that
A1:        M is complete;
  let a be Point of M such that
A2: ex b be Point of M st dist(a,b) <> 0;
  consider b be Point of M such that
A3:    dist(a,b)<>0  by A2;
A3':b<>a by A3,METRIC_1:1;
  let X be infinite set;
  set W=WellSpace(a,X);
  thus W is complete by A1,Th43;
  set TW=TopSpaceMetr W;
  consider f being Function of NAT, X such that 
A4: f is one-to-one by DICKSON:3;
  defpred p[set,set] means $2=[f.$1,b];
A5:for x st x in NAT ex y st y in the carrier of TW & p[x,y]
    proof
      let x such that 
    A6: x in NAT;
      take [f.x,b];
      x in dom f by A6,FUNCT_2:def 1;
      then f.x in rng f by FUNCT_1:def 5;
      hence thesis by A3',Th39;
    end;
  consider s be Function of NAT, the carrier of TW such that
A6:  for x st x in NAT holds p[x,s.x] from FUNCT_2:sch 1(A5);
  deffunc P(set)={s.$1};
A7:for x st x in NAT holds P(x) in bool(the carrier of TW)
    proof
      let x such that 
    A8: x in NAT;
      dom s=NAT by FUNCT_2:def 1;
      then s.x in rng s by A8,FUNCT_1:def 5;
      then P(x) is Subset of W by SUBSET_1:55;
      hence thesis;
    end;
  consider S be SetSequence of TW such that
A8: for x st x in NAT holds S.x=P(x) from FUNCT_2:sch 2(A7);
  now let x be set such that 
  A9: x in dom S;
     S.x={s.x} by A8,A9;
     hence S.x is non empty;
  end;then 
A10:S is non-empty by FUNCT_1:def 15;
  reconsider rngs=rng s as Subset of TW;
  set F={{x} where x is Element of TW: x in rngs};
  reconsider F as Subset-Family of TW by RELSET_2:16;
  rng S c= F
    proof
      let x such that 
    A11: x in rng S;
      consider y such that
    A12: y in dom S & S.y=x by A11,FUNCT_1:def 5;
      dom S=NAT & dom s=NAT by FUNCT_2:def 1;
      then x={s.y} & s.y in rngs by A8,A12,FUNCT_1:def 5;
      hence thesis;
    end;
  then consider R be non-empty closed SetSequence of TW such that
A11: R is descending and
A12: F is locally_finite & S is one-to-one implies meet R = {} and
A13: for i ex Si be Subset-Family of TW st
             R.i = Cl union Si &
             Si = {S.j where j is Element of NAT: j >= i} by  A10,Th24;
  reconsider R'=R as non-empty SetSequence of W;
  dist(a,b)>0 by A3,METRIC_1:5;then 
A15: 2*dist(a,b)>0  by XREAL_1:131;
A16:now let x,y be Point of W such that A17:x in rngs & y in rngs & x <> y;
     consider x1 be set such that
   A18: x1 in dom s & s.x1=x by A17,FUNCT_1:def 5;
     consider y1 be set such that
   A19: y1 in dom s & s.y1=y by A17,FUNCT_1:def 5;
     x=[f.x1,b] & y=[f.y1,b] by A6,A18,A19;
     then well_dist(a,X).(x,y)=dist(b,a)+dist(a,b) by A17,def10;
     hence dist(x,y)=2*dist(a,b);
  end;
  now let i;
     consider Si be Subset-Family of TW such that
  A17: R.i = Cl union Si and
  A18: Si = {S.j where j is Element of NAT: j >= i} by A13;
     reconsider SI=union Si,CLR=Cl union Si  as Subset of W;
     now let x,y being Point of W such that
     A19: x in SI & y in SI;
        consider xS be set such that
     A20: x in xS & xS in Si by A19,TARSKI:def 4;
        consider yS be set such that
     A21: y in yS & yS in Si by A19,TARSKI:def 4;
        consider j1 be Element of NAT such that 
     A22: xS=S.j1 & j1 >= i by A18,A20;
        consider j2 be Element of NAT such that 
     A23: yS=S.j2 & j2 >= i by A18,A21;
        dom s=NAT & dom S=NAT by FUNCT_2:def 1;
        then s.j1 in rngs & S.j1={s.j1} & s.j2 in rngs & S.j2={s.j2} 
          by A8,FUNCT_1:def 5; 
        then x in rngs & y in rngs & (x=y or x<>y)
          by A20,A21,A22,A23,TARSKI:def 1;       
        hence dist(x,y)<=2*dist(a,b) by A15,A16,METRIC_1:1;
     end;
     then SI is bounded by A15,TBSP_1:def 9;
     hence R'.i is bounded by A17,Th9;
  end;
  then reconsider R' as non-empty bounded SetSequence of W by def1;
  take R';
  thus R' is closed & R' is descending by A11,Th8;
A17:for x,y be Point of W st x<>y & x in rngs & y in rngs  holds
  dist(x,y)>=2*dist(a,b) by A16;
  now let x1,x2 be set such that 
  A18: x1 in NAT & x2 in NAT & S.x1 = S.x2;
     S.x1={s.x1} & S.x2={s.x2} & s.x1 in {s.x1} by A8,A18,TARSKI:def 1;
     then s.x1=s.x2 & s.x1=[f.x1,b] & s.x2=[f.x2,b] by A6,A18,TARSKI:def 1;
     then f.x1=f.x2 by ZFMISC_1:33;
     hence x1 = x2 by A4,A18,FUNCT_2:25;
  end;
  hence thesis by A12,A17,FUNCT_2:25,A15,LocallyFinite;
end;

theorem 
  ex M be non empty MetrSpace st 
    M is complete & 
    ex S be non-empty bounded SetSequence of M st
      S is closed & S is descending & meet S is empty
proof
  reconsider D=DiscreteSpace 2 as non empty MetrSpace;
  reconsider a=0,b=1 as Point of D by EULER_1:1;
A1:1=dist(a,b) by METRIC_1:def 11;
  TopSpaceMetr D is compact by COMPTS_1:27;
  then D is complete & NAT is infinite by TBSP_1:10,CARD_4:15;
  then WellSpace(a,NAT) is complete & 
  ex S be non-empty bounded SetSequence of WellSpace(a,NAT) st
     S is closed & S is descending & meet S is empty by A1,Th44;
  hence thesis;
end;