:: 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, ZF_REFLE, RELAT_2, ABSVALUE, FINSET_1, TARSKI, BHSP_3, TBSP_1,
      URYSOHN1, CARD_1, RLVECT_3, PARTFUN1, WELLORD1, METRIC_6, TOPGEN_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, ZFMISC_1, XXREAL_0, XREAL_0, REAL_1,
      SETFAM_1, DOMAIN_1, STRUCT_0, PRE_TOPC, TOPS_2, COMPTS_1, RELAT_1,
      FUNCT_1, VALUED_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, NAT_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, SEQ_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, XXREAL_0, YELLOW13, CARD_1, ORDERS_2, XBOOLE_0, VALUED_1,
      FUNCT_2, NUMBERS, FINSET_1;
 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,
      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, DICKSON,
      RELSET_2, TOPGEN_1, WELLFND1, CARD_FIL, WAYBEL23, UNIFORM1,
      CARD_2, TOPREAL6;
 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
A4: for n being Element of NAT holds S.n = F(n) from KURATO_2:sch 1;
    take S;
A5: now
      let i;
      reconsider i'=i as Element of NAT by ORDINAL1:def 13;
      X is bounded & S.i'=F(i) by A2,A4,TBSP_1:def 9;
      hence S.i is bounded;
    end;
    for x st x in dom S holds S.x is non empty by A4;
    hence thesis by A5,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;
    end;
    consider f be Function of NAT,REAL such that
A3: 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 A3;
  end;
  uniqueness
  proof
    let D1,D2 be Real_Sequence such that
A4: for i holds D1.i = diameter S.i and
A5: for i holds D2.i = diameter S.i;
    now
      let x such that
A6:   x in NAT;
      reconsider i=x as Element of NAT by A6;
      thus D1.x = diameter S.i by A4
        .= D2.x by A5;
    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,Def1,Def2,KURATO_2:22;
    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 A1,A3,Def1,Def2,KURATO_2:22;
    hence d.n<=d.m by TBSP_1:32;
  end;
  hence thesis by A2,SEQM_3:def 4,SEQ_2:def 3;
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 A1,A2,Def1,Def2,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
A6: dist(F.m1,F.m2)<=d.n & 0 <= d.n & abs(d.n-0)<r by A4,TBSP_1:29,def 10;
  then d.n < r by ABSVALUE:def 1;
  hence thesis by A6,XXREAL_0:2;
end;

theorem Th5:
  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 TOPREAL6:67;
  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 METRIC_1:4,XREAL_1:9;
    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
    TopSpaceMetr(M) = TopStruct (#the carrier of M,Family_open_set M#);
    then {} in Family_open_set M by PRE_TOPC:5;
    then
X:     {}M is open by Def3;
    ({}M)``= {}M;
    then {}M=([#]M)`;
    then ({}M)` is closed by Def4,X;
    hence thesis;
  end;
end;

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

Lm1: 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;
  for x st x in dom S holds S.x is non empty by A1,A3;
  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 Lm1;
    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 Lm1;
    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 Lm1;
    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 Lm1;
    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 ORDINAL1:def 13,TBSP_1:19;
      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
A6: x in the carrier of M by XBOOLE_0:def 1;
    reconsider x as Point of M by A6;
    set B=cl_Ball(x,1);
    deffunc F(set)=B;
    consider S being SetSequence of M such that
A7: for n being Element of NAT holds S.n = F(n) from KURATO_2:sch 1;
    take S;
A8: now
      let i;
      B is bounded & i in NAT by ORDINAL1:def 13,TOPREAL6:67;
      hence S.i is bounded by A7;
    end;
A9: now
      let y such that
A10:  y in dom S;
      reconsider n=y as Element of NAT by A10;
      dist(x,x)=0 by METRIC_1:1;
      then x in B & B=S.n by A7,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 A7,Def3;
      hence S.i is closed by Def4;
    end;
    hence thesis by A8,A9,Def1,Def8,FUNCT_1:def 15;
  end;
end;

theorem Th7:
  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,Th6;
  end;
  thus S' is open implies S is open
  proof
    assume
A3: S' is open;
    let i;
    S'.i is open by A3,Def5;
    hence thesis by A1,Th6;
  end;
  thus S is closed implies S' is closed
  proof
    assume
A4: S is closed;
    let i;
    S.i is closed by A4,Def8;
    hence thesis by A1,Th6;
  end;
  assume
A5: S' is closed;
  let i;
  S'.i is closed by A5,Def6;
  hence thesis by A1,Th6;
end;

theorem Th8:
  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;
A5: d+1>0+0 by A1,TBSP_1:29,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,METRIC_1:12,TBSP_1:def 10;
      then dist(x,y1)<=dist(x,x1)+dist(x1,y1) & dist(x,x1)+dist(x1,y1)<dd2+ d
      & dist(y1,y) < dd2 by METRIC_1:4,XREAL_1:10;
      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,METRIC_1:4,XREAL_1:10;
      hence contradiction;
    end;
    now
      let x,y be Point of M such that
A14:  x in CL & y in CL;
      dist(x,y)<=d & d+0<d+1 by A6,A14,XREAL_1:10;
      hence dist(x,y) <= d+1 by XXREAL_0:2;
    end;
    then
A15: CL is bounded by A5,TBSP_1:def 9;
    now
      let s such that
A16:  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
A17:    x in S & y in S;
        S c= CL by A2,PRE_TOPC:48;
        hence dist(x,y)<=s by A16,A17;
      end;
      hence d <= s by A1,A3,TBSP_1:def 10;
    end;
    hence thesis by A4,A6,A15,TBSP_1:def 10;
  end;
  suppose S={};
    hence thesis by A2,PCOMPS_1:2;
  end;
end;

begin :: Cantor's theorem on complete spaces

theorem Th9:
  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
A4: for x st x in NAT holds P[x,S.x] from FUNCT_2:sch 1(A1);
A5: now
    let x such that
A6: x in dom S;
    reconsider i=x as Element of NAT by A6;
    consider U be Subset of T such that
A7: U={C.j where j is Element of NAT: j >= i} & S.i=Cl U by A4;
    C.i in U & U c= S.i by A7,PRE_TOPC:48;
    hence S.x is non empty;
  end;
  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 A4;
    hence S.i is closed by Th6;
  end;
  then reconsider S as non-empty closed SetSequence of M
  by A5,Def8,FUNCT_1:def 15;
  take S;
  now
    let i be Element of NAT;
    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 A4;
    consider U1 be Subset of T such that
A9: U1={C.j where j is Element of NAT: j >= i+1} & S.(i+1)=Cl U1 by A4;
    U1 c= U
    proof
      let x such that
A10:  x in U1;
      consider j be Element of NAT such that
A11:  x=C.j & j>=i+1 by A9,A10;
      j>= i by A11,NAT_1:13;
      hence thesis by A8,A11;
    end;
    hence S.(i+1) c= S.i by A8,A9,PRE_TOPC:49;
  end;
  hence
A12: S is descending by KURATO_2:def 5;
  thus C is Cauchy implies S is bounded & lim diameter S = 0
  proof
    assume
A13: C is Cauchy;
A14: now
      let i;
      i in NAT by ORDINAL1:def 13;
      then consider U be Subset of T such that
A15:  U={C.j where j is Element of NAT: j >= i} & S.i=Cl U by A4;
      reconsider U'=U as Subset of M;
      U c= rng C
      proof
        let x such that
A16:    x in U;
        dom C=NAT & ex j be Element of NAT st x=C.j & j>=i
        by A15,A16,FUNCT_2:def 1;
        hence thesis by FUNCT_1:def 5;
      end;
      then U' is bounded by A13,TBSP_1:21,34;
      hence S.i is bounded by A15,Th8;
    end;
    hence S is bounded by Def1;
    reconsider S'=S as non-empty bounded closed SetSequence of M by A14,Def1;
    set d=diameter S';
    d is bounded_below & d is non-increasing by A12,Th1,Th2;
    then
A17: 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
A18:  0<r;
      reconsider R=r as Real by XREAL_0:def 1;
      set R2=R/2;
      R2>0 by A18,XREAL_1:141;
      then consider p be Element of NAT such that
A19:  for n,m be Element of NAT st p<=n & p<=m holds
      dist(C.n,C.m)<R2 by A13,TBSP_1:def 5;
      take p;
      let m be Element of NAT such that
A20:  p<=m;
      consider U be Subset of T such that
A21:  U={C.j where j is Element of NAT: j >= m} & S.m=Cl U by A4;
      reconsider U'=U as Subset of M;
A22:  U c= rng C
      proof
        let x such that
A23:    x in U;
        dom C=NAT & ex j be Element of NAT st x=C.j & j>=m
        by A21,A23,FUNCT_2:def 1;
        hence thesis by FUNCT_1:def 5;
      end;
A24:  rng C is bounded & C.m in U by A13,A21,TBSP_1:34;
      then
A25:  U' is bounded & U' is non empty by A22,TBSP_1:21;
      now
        let x,y being Point of M such that
A26:    x in U' & y in U';
        consider i be Element of NAT such that
A27:    x = C.i & i>=m by A21,A26;
        consider j be Element of NAT such that
A28:    y=C.j & j>=m by A21,A26;
        i>=p & j>=p by A20,A27,A28,XXREAL_0:2;
        hence dist(x,y)<=R2 by A19,A27,A28;
      end;
      then diameter U'<=R2 & diameter U'=diameter S.m
      by A21,A25,Th8,TBSP_1:def 10;
      then diameter S.m <= R2 & diameter S.m>=0 by A22,A24,TBSP_1:21,29;
      then abs(diameter S.m)<=R2 & R2<R by A18,ABSVALUE:def 1,XREAL_1:218;
      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 A17,SEQ_2:def 7;
  end;
  let i;
  i in NAT by ORDINAL1:def 13;
  hence thesis by A4;
end;

theorem Th10:
  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
A7: 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 A7;
    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
A8: 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
A9:   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
A10:  Si is closed by Th6;
      rng F1 c= Si
      proof
        let x such that
A11:    x in rng F1;
        consider y such that
A12:    y in dom F1 & F1.y=x by A11,FUNCT_1:def 5;
        reconsider y as Element of NAT by A12;
        x=F.(y+i) & i<=y+i by A9,A12,NAT_1:11;
        then x in S.(y+i) & S.(y+i) c= S.i by A2,A7,KURATO_2:22;
        hence thesis;
      end;
      then
A13:  Lim F1 c= Si by A10,FRECHET2:12;
      F' is_convergent_to x' by A8,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 A13;
    end;
    hence thesis by KURATO_2:6;
  end;
  assume
A14: 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
A15: F is Cauchy;
  consider S be non-empty closed SetSequence of M such that
A16: S is descending and
A17: F is Cauchy implies S is bounded & lim diameter S = 0 and
A18: 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 Th9;
  meet S is non empty by A14,A15,A16,A17;
  then consider x such that
A19: x in meet S by XBOOLE_0:def 1;
  reconsider x as Point of M by A19;
  take x;
  let r such that
A20: r>0;
  set d=diameter S;
  d is bounded_below & d is non-increasing by A15,A16,A17,Th1,Th2;
  then d is convergent by SEQ_4:52;
  then consider n be Element of NAT such that
A21: for m be Element of NAT st n<=m holds abs(d.m-0)<r by A15,A17,A20,
  SEQ_2:def 7;
  take n;
  let m be Element of NAT such that
A22: n<=m;
  consider U be Subset of T such that
A23: U = { F.j where j is Element of NAT: j >= m } & S.m = Cl U by A18;
  F.m in U & U c= Cl U by A23,PRE_TOPC:48;
  then x in S.m & F.m in S.m & S.m is bounded by A15,A17,A19,A23,Def1,
  KURATO_2:6;
  then dist(F.m,x) <= diameter (S.m) & diameter (S.m)>=0 & diameter (S.m)=d.m
  & abs(d.m-0)<r by A21,A22,Def2,TBSP_1:29,def 10;
  then dist(F.m,x) <= d.m & d.m <r by ABSVALUE:def 1;
  hence thesis by XXREAL_0:2;
end;

theorem Th11:
  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
A7: for x st x in G holds P[x,f.x] from FUNCT_2:sch 1(A5);
A8: dom f=G by FUNCT_2:def 1;
    rng f is finite by A4;
    then consider i be Element of NAT such that
A9: 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
A10: x in S.i by XBOOLE_0:def 1;
    now
      let Y be set;
      assume
A11:  Y in G;
      then
A12:  f.Y in rng f by A8,FUNCT_1:def 5;
      then reconsider fY=f.Y as Element of NAT;
      Y=S.fY & fY <= i by A7,A9,A11,A12;
      then S.i c= Y by A1,KURATO_2:22;
      hence x in Y by A10;
    end;
    hence meet G<>{} by A4,SETFAM_1:def 1;
  end;
  hence thesis by A3,COMPTS_1:def 2;
end;

theorem Th12:
  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;
    S.x is open by A2,Def7;
    hence thesis by A3,Th6;
  end;
  assume
A4: S is closed;
  let P be Subset of T;
  assume P in F;
  then consider x such that
A5: x in dom S & S.x=P by A1,FUNCT_1:def 5;
  reconsider x as natural number by A5;
  S.x is closed by A4,Def8;
  hence thesis by A5,Th6;
end;

theorem Th13:
  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};
A5: for x st x in NAT ex y st y in bool(the carrier of T) & P[x,y]
  proof
    let x such that
A6: x in NAT;
    reconsider i=x as Element of NAT by A6;
    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
A7: for x st x in NAT holds P[x,R.x] from FUNCT_2:sch 1(A5);
A8: 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};
A9: i+1 is finite;
    deffunc F(set)=S.$1;
A10: {F(j)where j is Element of NAT:j in i+1} is finite
    from FRAENKEL:sch 21(A9);
    SS c= {F(j)where j is Element of NAT:j in i+1}
    proof
      let x such that
A11:  x in SS;
      consider j be Element of NAT such that
A12:  x=S.j & j<=i by A11;
      j<i+1 by A12,NAT_1:13;
      then j in i+1 by EULER_1:1;
      hence thesis by A12;
    end;
    hence thesis by A10;
  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};
A13: S.0 in SS;
    SS c= S1
    proof
      let x such that
A14:  x in SS;
      consider j be Element of NAT such that
A15:  x=S.j & j<=i by A14;
      j<=i+1 by A15,NAT_1:13;
      hence thesis by A15;
    end;
    then meet S1 c= meet SS & meet SS=R.i by A7,A13,SETFAM_1:7;
    hence R.(i+1) c= R.i by A7;
  end;
  hence R is descending by KURATO_2:def 5;
  thus F is centered implies R is non-empty
  proof
    assume
A16: F is centered;
    now
      let x such that
A17:  x in dom R;
      reconsider i=x as Element of NAT by A17;
      set SS={S.j where j is Element of NAT:j<=i};
      SS is finite & S.0 in SS & SS c= F by A2,A8;
      then meet SS<>{} by A16,COMPTS_1:def 2;
      hence R.x is non empty by A7;
    end;
    hence thesis by FUNCT_1:def 15;
  end;
  thus F is open implies R is open
  proof
    assume
A18: F is open;
    let i;
    set SS={S.j where j is Element of NAT:j<=i};
A19: 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 A8,A18,A19,ORDINAL1:def 13,TOPS_2:18;
    then meet SS is open & R.i=meet SS by A7,TOPS_2:27;
    hence thesis;
  end;
  thus F is closed implies R is closed
  proof
    assume
A20: F is closed;
    let i;
    set SS={S.j where j is Element of NAT:j<=i};
A21: SS c= F by A2;
    then reconsider SS as Subset-Family of T by XBOOLE_1:1;
    SS is closed & i in NAT by A20,A21,ORDINAL1:def 13,TOPS_2:19;
    then meet SS is closed & meet SS=R.i by A7,TOPS_2:29;
    hence thesis;
  end;
  let i;
  i in NAT by ORDINAL1:def 13;
  hence thesis by A7;
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;
      consider A be Subset of M such that
A6:   A in F & A is bounded & diameter A < 1/(i+1) by A3,XREAL_1:141;
      take A;
      thus thesis by A6;
    end;
    consider f be SetSequence of M such that
A7: for x st x in NAT holds P[x,f.x] from FUNCT_2:sch 1(A4);
    rng f c= F
    proof
      let x such that
A8:   x in rng f;
      consider y such that
A9:   y in dom f & f.y=x by A8,FUNCT_1:def 5;
      reconsider y as Element of NAT by A9;
      f.y in F by A7;
      hence thesis by A9;
    end;
    then consider R be SetSequence of T such that
A10: R is descending and
A11: F is centered implies R is non-empty and F is open implies R is open and
A12: F is closed implies R is closed and
A13: for i holds R.i = meet {f.j where j is Element of NAT: j<=i} by Th13;
    reconsider R'=R as non-empty SetSequence of M by A2,A11;
    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 A7,A13;
      hence R'.i is bounded by TBSP_1:21;
    end;
    then reconsider R' as non-empty bounded SetSequence of M by Def1;
A14: R' is closed & R' is descending by A2,A10,A12,Th7;
    deffunc F(Element of NAT)=1/(1+$1);
    consider seq be Real_Sequence such that
A15: 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 A15;
    then
A16: seq is convergent & lim seq=0 by SEQ_4:45;
    then
A17: 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 A13;
      then R.n c= f.n & f.n is bounded by A7,SETFAM_1:4;
      then diameter R'.n <= diameter f.n & diameter f.n < F(n)&R'.n is bounded
      by A7,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 A15,Def2,SEQ_1:13,TBSP_1:29,XXREAL_0:2;
      hence Ns.n <= dR.n & dR.n<=seq.n;
    end;
    then
A18: dR is convergent & lim dR=0 by A16,A17,SEQ_2:33,34;
    then meet R'<>{} by A1,A14,Th10;
    then consider x0 be set such that
A19: x0 in meet R' by XBOOLE_0:def 1;
    reconsider x0 as Point of M by A19;
A20: now
      let y;
      assume
A21:  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;
A22:  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
A23:    x in NAT;
        reconsider i=x as Element of NAT by A23;
        take R.i/\Y;
        thus thesis;
      end;
      consider f' be SetSequence of M such that
A24:  for x st x in NAT holds P'[x,f'.x] from FUNCT_2:sch 1(A22);
A25:  now
        let x such that
A26:    x in dom f';
        reconsider i=x as Element of NAT by A26;
        set SS={f.j where j is Element of NAT:j<=i};
A27:    Y in {Y} & f.i in SS by TARSKI:def 1;
A28:    {Y}\/SS c= F
        proof
          let z be set such that
A29:      z in {Y}\/SS;
          per cases by A29,XBOOLE_0:def 2;
          suppose z in {Y};
            hence thesis by A21,TARSKI:def 1;
          end;
          suppose z in SS;
            then ex j be Element of NAT st z=f.j & j<=i;
            hence thesis by A7;
          end;
        end;
A30:    i+1 is finite;
        deffunc F(set)=f.$1;
A31:    {F(j)where j is Element of NAT:j in i+1} is finite
        from FRAENKEL:sch 21(A30);
        SS c= {F(j) where j is Element of NAT:j in i+1}
        proof
          let x such that
A32:      x in SS;
          consider j be Element of NAT such that
A33:      x=f.j & j<=i by A32;
          j<i+1 by A33,NAT_1:13;
          then j in i+1 by EULER_1:1;
          hence thesis by A33;
        end;
        then SS is finite by A31;
        then {Y}\/SS is finite;
        then meet({Y}\/SS)<>{} by A2,A28,COMPTS_1:def 2;
        then meet {Y} /\ meet SS <> {} by A27,SETFAM_1:10;
        then Y /\meet SS<>{} by SETFAM_1:11;
        then Y/\R.i<>{} by A13;
        hence f'.x is non empty by A24;
      end;
A34:  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 A24,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 A14,Def8;
        then Ri is closed & Y is closed & i in NAT
        by A2,A21,Th6,ORDINAL1:def 13,TOPS_2:def 2;
        then Ri/\Y is closed & f'.i=Ri/\Y by A24,TOPS_1:35;
        hence f'.i is closed by Th6;
      end;
      then reconsider f' as non-empty bounded closed SetSequence of M
      by A25,A34,Def1,Def8,FUNCT_1:def 15;
      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 A10,A24,KURATO_2:def 5;
        hence f'.(i+1) c= f'.i by XBOOLE_1:26;
      end;
      then
A35:  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 A24,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 Def2,SEQ_1:13,TBSP_1:29;
        hence Ns.n <= df.n & df.n<=dR.n by Def2;
      end;
      then lim df=0 by A17,A18,SEQ_2:34;
      then meet f'<>{} by A1,A35,Th10;
      then consider z be set such that
A36:  z in meet f' by XBOOLE_0:def 1;
      reconsider z as Point of M by A36;
A37:  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
A38:    for j be Element of NAT st i<=j holds
        abs(dR.j-0)<dist(x0,z) by A18,SEQ_2:def 7;
        z in f'.i & f'.i=R.i/\Y by A24,A36,KURATO_2:6;
        then z in R.i & x0 in R.i & R'.i is bounded
        by A19,Def1,KURATO_2:6,XBOOLE_0:def 3;
        then dist(x0,z)<=diameter (R'.i) & 0<=diameter (R'.i)
        by TBSP_1:29,def 10;
        then abs(diameter (R'.i))>=dist(x0,z) & abs(dR.i-0)<dist(x0,z)
        by A38,ABSVALUE:def 1;
        hence thesis by Def2;
      end;
      z in f'.0 & f'.0=R.0/\Y by A24,A36,KURATO_2:6;
      hence x0 in y by A37,XBOOLE_0:def 3;
    end;
    F<>{} by A2,COMPTS_1:def 2;
    hence thesis by A20,SETFAM_1:def 1;
  end;
  assume
A39: 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
A40: S is descending & lim diameter S = 0;
    reconsider RS=rng S as Subset-Family of T;
A41: RS is closed & RS is centered by A40,Th11,Th12;
    now
      let r such that
A42:  r > 0;
      set d=diameter S;
      d is bounded_below & d is non-increasing by A40,Th1,Th2;
      then d is convergent by SEQ_4:52;
      then consider n be Element of NAT such that
A43:  for m be Element of NAT st n<=m holds abs(d.m-0)<r
      by A40,A42,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 A43,Def2,FUNCT_2:def 1,TBSP_1:29;
      hence Sn in RS & Sn is bounded & diameter Sn <r
      by Def1,ABSVALUE:def 1,FUNCT_1:def 5;
    end;
    then meet RS is non empty by A39,A41;
    then consider x such that
A44: 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 FUNCT_1:def 5,RELAT_1:65;
      hence x in S.i by A44,SETFAM_1:def 1;
    end;
    hence meet S is non empty by KURATO_2:6;
  end;
  hence thesis by Th10;
end;

theorem Th15:
  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
A3: B is bounded;
  per cases;
  suppose B'={}(M|A);
    hence thesis;
  end;
  suppose B'<>{}(M|A);
    then consider p be set such that
A4: p in B' by XBOOLE_0:def 1;
    reconsider p as Point of (M|A) by A4;
A5: 0+0 < diameter B+1 by A3,TBSP_1:29,XREAL_1:10;
    now
      let q be Point of (M|A) such that
A6:   q in B';
      reconsider p'=p,q'=q as Point of M by TOPMETR:12;
A7:   dist(p,q) = dist(p',q') by TOPMETR:def 1;
      dist(p',q')<=diameter B & diameter B+0<=diameter B+1
      by A1,A3,A4,A6,TBSP_1:def 10,XREAL_1:10;
      hence dist(p,q)<=diameter B+1 by A7,XXREAL_0:2;
    end;
    hence thesis by A4,A5,TBSP_1:15;
  end;
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' & 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,Th15;
  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 Th17:
  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 Th18:
  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
A6: S is Cauchy;
  let r such that
A7: r>0;
  consider p be Element of NAT such that
A8: for n,m be Element of NAT st p<=n & p<=m holds
  dist(S.n,S.m)<r by A6,A7,TBSP_1:def 5;
  take p;
  let n,m be Element of NAT such that
A9: p <= n & p <= m;
  dist(S.n,S.m) = dist(S'.n,S'.m) by A1,TOPMETR:def 1;
  hence thesis by A8,A9;
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
A8:   for x st x in NAT holds P[x,f.x] from FUNCT_2:sch 1(A6);
A9:   now
        let x such that
A10:    x in dom f;
        reconsider i=x as Element of NAT by A10;
        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
A11:    y in B & y in A' by XBOOLE_0:3;
        reconsider y as Point of M by A11;
        dist(p,y)< 1/(i+1) by A11,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,A11,XBOOLE_0:def 3;
        hence f.x is non empty by A8;
      end;
A12:  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 TOPREAL6:67,XBOOLE_1:17;
        then
A13:    ACL is bounded by TBSP_1:21;
        i in NAT by ORDINAL1:def 13;
        then f.i=ACL by A8;
        hence f.i is bounded by A13,Th15;
      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
A14:    cB is closed by TOPS_1:29;
        reconsider fi=f.i as Subset of TA;
A15:    TA=T|A' by A2,HAUSDORF:18;
        then [#](T|A')=A & i in NAT by ORDINAL1:def 13,TOPMETR:def 2;
        then fi=cB/\[#](T|A') by A8;
        then fi is closed by A14,A15,PRE_TOPC:43;
        hence f.i is closed by Th6;
      end;
      then reconsider f as non-empty bounded closed SetSequence of MA
      by A9,A12,Def1,Def8,FUNCT_1:def 15;
      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
A16:      x in cl_Ball(p,1/(i1+1));
          reconsider q=x as Point of M by A16;
          i1<i1+1 by NAT_1:13;
          then dist(p,q)<=1/(i1+1) & 1/(i1+1)<1/i1
          by A16,METRIC_1:13,XREAL_1:78;
          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 A8,XBOOLE_1:26;
        hence f.(i+1) c= f.i by A8;
      end;
      then
A17:  f is descending by KURATO_2:def 5;
      deffunc F(Element of NAT)=1/(1+$1);
      consider seq be Real_Sequence such that
A18:  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 A18;
      then
A19:  seq is convergent & lim seq=0 by SEQ_4:45;
      then
A20:  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));
A21:    cB is bounded & diameter cB <= 2*F(n) & A/\cB c= cB
        by Th5,TOPREAL6:67,XBOOLE_1:17;
        then A/\cB is bounded & diameter(A/\cB)<= diameter cB & f.n=A/\cB
        by A8,TBSP_1:21,32;
        then diameter(A/\cB)<=2*F(n) & diameter (f.n) <= diameter(A/\cB)&
        f.n is bounded by A21,Th15,Th16,XXREAL_0:2;
        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 A18,Def2,SEQ_1:13,TBSP_1:29,XXREAL_0:2;
        hence Ns.n <= df.n & df.n<=Ts.n;
      end;
      then lim df = 0 & df is convergent by A20,SEQ_2:33,34;
      then meet f is non empty by A3,A17,Th10;
      then consider q be set such that
A22:  q in meet f by XBOOLE_0:def 1;
      reconsider q as Point of M by A22,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
A23:    for m be Element of NAT st n<=m holds abs(seq.m-0)<dist(p,q)
        by A19,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 A8,A18,A22,KURATO_2:6;
        then q in cB & abs(seq.n-0)=F(n) by ABSVALUE:def 1,XBOOLE_0:def 3;
        then dist(p,q) <= F(n) & F(n) < dist(p,q) by A23,METRIC_1:13;
        hence thesis;
      end;
      then f.0=A/\cl_Ball(p,1/(0+1)) & p in f.0 by A8,A22,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
A24: A' is closed;
  let S be sequence of MA such that
A25: S is Cauchy;
  reconsider S'=S as sequence of M by Th17;
  S' is Cauchy by A25,Th18;
  then
A26: S' is convergent by A1,TBSP_1:def 6;
A27: 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 A24,A26,A27,TOPMETR3:2;
  take limS;
  let r such that
A28: r>0;
  consider n be Element of NAT such that
A29: for m be Element of NAT st m>=n holds
  dist(S'.m,lim S')<r by A26,A28,TBSP_1:def 4;
  take n;
  let m be Element of NAT such that
A30: m>=n;
  dist(S.m,limS) = dist(S'.m,lim S') by TOPMETR:def 1;
  hence thesis by A29,A30;
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 Cover of T & F is open & F is countable ex G being Subset-Family of T
  st G c= F & G is Cover of T & G is finite;
end;

theorem Th20:
  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 Cover of T & F is open & F is countable;
  thus thesis by A1,A2,COMPTS_1:def 3;
end;

theorem Th21:
  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 Cover of T & COMPLEMENT(F) is open &
    COMPLEMENT(F) is countable by A2,A3,SETFAM_1:60,TOPGEN_4:1,TOPS_2:16;
    then consider G' be Subset-Family of T such that
A5: G' c= COMPLEMENT(F) & G' is 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;
A9: G' <> {} by A5,TOPS_2:5;
A10: meet COMPLEMENT(G') = (union G')` by A5,TOPS_2:5,11
      .= ([#] T) \ ([#] T) by A5,SETFAM_1:60
      .= {} by XBOOLE_1:37;
    COMPLEMENT(G') <> {} & COMPLEMENT(G') is finite by A6,A9,TOPS_2:10,13;
    hence contradiction by A2,A7,A10,COMPTS_1:def 2;
  end;
  assume
A11: 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
A12: F is Cover of T & F is open and
A13: F is countable;
A14: COMPLEMENT(F) is countable & COMPLEMENT(F) is closed &
  F <> {} by A12,A13,TOPGEN_4:1,TOPS_2:5,17;
  then meet COMPLEMENT(F) = (union F)` by TOPS_2:11
    .= ([#] T) \ ([#] T) by A12,SETFAM_1:60
    .= {} by XBOOLE_1:37;
  then COMPLEMENT(F) <> {} & not COMPLEMENT(F) is centered
  by A11,A14,TOPS_2:10;
  then consider G' being set such that
A15: G' <> {} & G' c= COMPLEMENT(F) and
A16: G' is finite & meet G' = {} by COMPTS_1:def 2;
  reconsider G' as Subset-Family of T by A15,XBOOLE_1:1;
  take F'=COMPLEMENT(G');
  thus F' c= F
  proof
    let x such that
A17: x in F';
    reconsider x'=x as Subset of T by A17;
    x'` in G' by A17,SETFAM_1:def 8;
    then x'`` in F by A15,SETFAM_1:def 8;
    hence x in F;
  end;
  union F' = (meet G')` by A15,TOPS_2:12
    .= [#] T by A16;
  hence thesis by A16,SETFAM_1:60,TOPS_2:13;
end;

theorem Th22:
  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
A3: rngS is centered & rngS is countable by A2,Th11,CARD_4:45;
    now
      let D be Subset of T such that
A4:   D in rngS;
      consider x such that
A5:   x in dom S & S.x=D by A4,FUNCT_1:def 5;
      reconsider x as Element of NAT by A5;
      S.x is closed by Def6;
      hence D is closed by A5;
    end;
    then rngS is closed by TOPS_2:def 2;
    then meet rngS<>{} by A1,A3,Th21;
    then consider x such that
A6: 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 A6,SETFAM_1:def 1;
    end;
    hence thesis by KURATO_2:6;
  end;
  assume
A7: 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
A8: F is centered & F is closed and
A9: F is countable;
A10: Card F c= omega by A9,CARD_4:def 1;
    now per cases by A10,CARD_1:13;
      suppose Card F = omega;
        then NAT,F are_equipotent by CARD_1:21,84;
        then consider s be Function such that
A11:    s is one-to-one & dom s = NAT & rng s = F by WELLORD2:def 4;
        reconsider s as SetSequence of T by A11,FUNCT_2:4;
        consider R be SetSequence of T such that
A12:    R is descending and
A13:    F is centered implies R is non-empty and
        F is open implies R is open and
A14:    F is closed implies R is closed and
A15:    for i holds R.i=meet{s.j where j is Element of NAT:j<=i}by A11,Th13;
        meet R<>{} by A7,A8,A12,A13,A14;
        then consider x such that
A16:    x in meet R by XBOOLE_0:def 1;
A17:    F is non empty by A11,RELAT_1:65;
        now
          let y;
          assume y in F;
          then consider z be set such that
A18:      z in dom s & s.z=y by A11,FUNCT_1:def 5;
          reconsider z as Element of NAT by A18;
          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 A15;
          then R.z c= s.z & x in R.z by A16,KURATO_2:6,SETFAM_1:4;
          hence x in y by A18;
        end;
        hence meet F is non empty by A17,SETFAM_1:def 1;
      end;
      suppose Card F in omega;
        then F is finite & F<>{} by A8,CARD_4:2,COMPTS_1:def 2;
        hence meet F is non empty by A8,COMPTS_1:def 2;
      end;
    end;
    hence meet F<>{};
  end;
  hence thesis by Th21;
end;

theorem Th23:
  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
A1: 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);
A2: for x st x in NAT ex y st y in bool(the carrier of T) & r[x,y]
  proof
    let x such that
A3: x in NAT;
    reconsider x'=x as Element of NAT by A3;
    set SS={S.j where j is Element of NAT:j >= x'};
    SS c= bool(the carrier of T)
    proof
      let y such that
A4:   y in SS;
      ex j be Element of NAT st S.j=y & j>=x' by A4;
      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 A1;
    end;
    hence thesis;
  end;
  consider R be SetSequence of T such that
A7: for x st x in NAT holds r[x,R.x] from FUNCT_2:sch 1(A2);
A8: now
    let n be set such that
A9: n in dom R;
    reconsider n'=n as Element of NAT by A9;
    consider SS be Subset-Family of T such that SS c= F and
A10: SS = {S.j where j is Element of NAT:j>=n'} & R.n'=Cl(union SS) by A7;
    dom S=NAT by FUNCT_2:def 1;
    then
A11: S.n'<>{} by A1,FUNCT_1:def 15;
    S.n' in SS by A10;
    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;
    hence R.n is non empty by A10,A11;
  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 A7;
    hence R.n is closed;
  end;
  then reconsider R as non-empty closed SetSequence of T
  by A8,Def6,FUNCT_1:def 15;
  take R;
  now
    let n be Element of NAT;
    consider Sn be Subset-Family of T such that Sn c= F and
A12: Sn = {S.j where j is Element of NAT:j>=n} and
A13: R.n=Cl(union Sn) by A7;
    consider Sn1 be Subset-Family of T such that Sn1 c= F and
A14: Sn1 = {S.j where j is Element of NAT:j>=n+1} and
A15: R.(n+1)=Cl(union Sn1) by A7;
    Sn1 c= Sn
    proof
      let y such that
A16:  y in Sn1;
      consider j be Element of NAT such that
A17:  y=S.j & j>=n+1 by A14,A16;
      j>=n by A17,NAT_1:13;
      hence thesis by A12,A17;
    end;
    then union Sn1 c= union Sn by ZFMISC_1:95;
    hence R.(n+1) c= R.n by A13,A15,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
A18: F is locally_finite & S is one-to-one;
    assume meet R <> {};
    then consider x such that
A19: x in meet R by XBOOLE_0:def 1;
    reconsider x as Point of T by A19;
A20: 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 A1,A18,PCOMPS_1:12;
    then consider W be Subset of T such that
A21: x in W & W is open and
A22: { V where V is Subset of T: V in rngS & V meets W } is finite
    by PCOMPS_1:def 2;
    reconsider Sp=S as Function of NAT,rngS by A20,FUNCT_2:3;
    reconsider S'=Sp" as Function;
    reconsider S' as Function of rngS,NAT by A18,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};
A23: Y is finite from FRAENKEL:sch 21(A22);
    Y c= NAT
    proof
      let y such that
A24:  y in Y;
      ex z be Element of rngS st y =s'(z) & z in X by A24;
      hence thesis;
    end;
    then reconsider Y as Subset of NAT;
    consider n be Element of NAT such that
A25: for k be Element of NAT st k in Y holds k <= n by A23,STIRL2_1:66;
    set n1=n+1;
    consider Sn be Subset-Family of T such that
A26: Sn c= F and
A27: Sn ={S.j where j is Element of NAT:j>=n1} and
A28: R.n1=Cl(union Sn) by A7;
    Sn is locally_finite by A18,A26,PCOMPS_1:12;
    then Cl(union Sn)=union(clf Sn) & x in R.n1 by A19,KURATO_2:6,PCOMPS_1:23;
    then consider CLF be set such that
A29: x in CLF & CLF in clf Sn by A28,TARSKI:def 4;
    reconsider CLF as Subset of T by A29;
    consider U be Subset of T such that
A30: CLF = Cl U & U in Sn by A29,PCOMPS_1:def 3;
    consider j be Element of NAT such that
A31: U=S.j & j>=n1 by A27,A30;
    Sp.j in rngS & Sp.j meets W by A21,A29,A30,A31,TOPS_1:39;
    then Sp.j in X & (S").(S.j) = j by A18,FUNCT_2:32;
    then j in Y;
    then j <=n by A25;
    hence thesis by A31,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 A7;
  hence thesis;
end;

Lm2: 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
A1: T is countably_compact;
  given F be Subset-Family of T such that
A2: F is locally_finite and
A3: F is with_non-empty_elements and
A4: F is infinite;
  consider f be Function of NAT, F such that
A5: f is one-to-one by A4,DICKSON:3;
A6: rng f c= F;
  reconsider f as SetSequence of T by A4,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 A3,A6,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 A6,Th23;
  hence thesis by A1,A2,A5,Th22;
end;

Lm3: 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:47;
  then F is with_non-empty_elements by SETFAM_1:def 9;
  hence thesis by A1,A2;
end;

Lm4: 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 A9,TARSKI:def 1,XBOOLE_0:def 3;
      hence thesis by A6,A8,A9;
    end;
    hence thesis by A5;
  end;
  now
    let a be Subset of T such that
A10: a in F;
    ex y be Point of T st a={y} & y in A by A10;
    hence Card a = 1 by CARD_1:50;
  end;
  then
A11: 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};
A12: PP is finite from FRAENKEL:sch 21(A11);
  A c= PP
  proof
    let y such that
A13: y in A;
    reconsider y'=y as Point of T by A13;
    {y'} in F & {y'} is Subset of T by A13;
    then P({y'}) in PP;
    hence thesis by SETFAM_1:11;
  end;
  hence thesis by A2,A12;
end;

theorem Th24:
  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
A5: Union g is finite by A1,A3,CARD_4:63;
A6: dom F c= Union g
  proof
    let x such that
A7: x in dom F;
    F.x in {F.x} & F.x in rng F by A7,FUNCT_1:def 5,TARSKI:def 1;
    then x in F"{F.x} & g.(F.x)=F"{F.x} & g.(F.x) in rng g
    by A3,A7,FUNCT_1:def 5,def 13;
    then x in union rng g by TARSKI:def 4;
    hence thesis by CARD_3:def 4;
  end;
  thus thesis by A1,A5,A6;
end;

theorem Th25:
  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;
  then consider x such that
A4: x in rng S & S"{x} is infinite by A3,Th24;
  now
    let n be Element of NAT;
    ex i st x in F.i & i >= n
    proof
      assume
A5:   for i st x in F.i holds i<n;
      S"{x} c= n
      proof
        let y such that
A6:     y in S"{x};
        reconsider i=y as Element of NAT by A6;
        S.i in {x} by A6,FUNCT_1:def 13;
        then S.i=x & S.i in F.i by A2,TARSKI:def 1;
        then i<n by A5;
        hence thesis by EULER_1:1;
      end;
      hence thesis by A4;
    end;
    then consider i such that
A7: x in F.i & i>=n;
    i in NAT by ORDINAL1:def 13;
    then F.i c= F.n by A1,A7,KURATO_2:22;
    hence x in F.n by A7;
  end;
  hence thesis by KURATO_2:6;
end;

Lm5: 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 Th22;
  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
A6: 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;
B7:  now
    let n;
    n in NAT by ORDINAL1:def 13;
    hence F.n in S.n by A6;
  end;
  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,B7,A2,Th25;
  then consider p be set such that
A8: p in Der rngF by XBOOLE_0:def 1;
  reconsider p as Point of T by A8;
  consider n be Element of NAT such that
A9: 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};
A10: n+1 is finite;
A11: F1n is finite from FRAENKEL:sch 21(A10);
  F1n c= the carrier of T
  proof
    let x such that
A12: x in F1n;
    ex i be Element of NAT st x=F.i & i in n+1 by A12;
    hence thesis;
  end;
  then reconsider F1n as Subset of T;
  set U=((S.n)`)\(F1n\{p});
  reconsider U as Subset of T;
  F1n\{p} is finite & (S.n) is closed by A11,Def6;
  then F1n\{p} is closed & (S.n)` is open;
  then
A13: U is open by FRECHET:4;
  p in {p} by TARSKI:def 1;
  then not p in F1n\{p} & p in (S.n)` by A9,XBOOLE_0:def 4;
  then p in U by XBOOLE_0:def 4;
  then consider q be Point of T such that
A14: q in rngF /\ U & q <> p by A8,A13,TOPGEN_1:19;
  q in rngF by A14,XBOOLE_0:def 3;
  then consider i be set such that
A15: i in dom F & F.i=q by FUNCT_1:def 5;
  reconsider i as Element of NAT by A15;
  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 A15;
    then q in F1n\{p} by A14,ZFMISC_1:64;
    then not q in U by XBOOLE_0:def 4;
    hence contradiction by A14,XBOOLE_0:def 3;
  end;
  suppose i>n;
    then q in S.i & S.i c= S.n by A2,A6,A15,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 A14,XBOOLE_0:def 3;
  end;
end;

Lm6: 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 Th22;
  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
A6: for x st x in NAT holds P[x,F.x] from FUNCT_2:sch 1(A3);
  now
    let n;
    n in NAT by ORDINAL1:def 13;
    hence F.n in S.n by A6;
  end;
  then
A7: rng F is infinite by A2,Th25;
  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;
A8: A is locally_finite
  proof
    let x be Point of T;
    consider i be Element of NAT such that
A9: 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 A9,SUBSET_1:50;
    deffunc f(set)={F.$1};
A10: i is finite;
    set SI={f(j) where j is Element of NAT:j in i};
A11: SI is finite from FRAENKEL:sch 21(A10);
    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
A12:  v in meetS;
      consider V be Subset of T such that
A13:  V=v & V in A & V meets Si' by A12;
      consider y be Point of T such that
A14:  V={y} & y in rng F by A13;
      consider z be set such that
A15:  z in dom F & y=F.z by A14,FUNCT_1:def 5;
      reconsider z as Element of NAT by A15;
      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,A6,A15,KURATO_2:22;
        then y in S.i & y in Si' by A13,A14,ZFMISC_1:56;
        hence thesis by XBOOLE_0:def 4;
      end;
      hence thesis by A13,A14,A15;
    end;
    hence meetS is finite by A11;
  end;
  now
    let a be Subset of T such that
A16: a in A;
    ex y be Point of T st a={y} & y in rngF by A16;
    hence Card a = 1 by CARD_1:50;
  end;
  then
A17: A is finite by A1,A8;
  deffunc P(set)=meet $1;
  set PP={P(y) where y is Element of bool(the carrier of T):y in A};
A18: PP is finite from FRAENKEL:sch 21(A17);
  rngF c= PP
  proof
    let y such that
A19: y in rngF;
    reconsider y'=y as Point of T by A19;
    {y'} in A & {y'} is Subset of T by A19;
    then P({y'}) in PP;
    hence thesis by SETFAM_1:11;
  end;
  hence thesis by A7,A18;
end;

theorem Th26:
  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 Lm2;
  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 Lm3;
  hence thesis by Lm6;
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 &
  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 Th26;
    hence thesis by Lm3;
  end;
  thus thesis by Lm6;
end;

theorem Th28:
  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 Th27;
    hence thesis by Lm4;
  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 Lm5;
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 Lm5,Th28;

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:8,def 5;
  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
A10:  ex q be Element of X() st q in union (rng f) & not P[p,q];
      take U=union (rng f);
      thus thesis by A10;
    end;
  end;
  consider h be Function of [:cRS,PFuncs(cRS, bX):],bX such that
A11: 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
A12: 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]);
A13: 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
A14: for y be Element of RS st y <> x & [y,x] in IRS holds S[y];
    set fIx=f|IRS-Seg x;
A15: union rng fIx c= IRS-Seg x
    proof
      let y be set such that
A16:  y in union rng fIx;
      consider z be set such that
A17:  y in z & z in rng fIx by A16,TARSKI:def 4;
      consider t be set such that
A18:  t in dom fIx & fIx.t=z by A17,FUNCT_1:def 5;
A19:  t in IRS-Seg x & IRS-Seg x c= cRS by A18,RELAT_1:86,WELLFND1:4;
      reconsider t as Element of RS by A18;
      t<>x & [t,x] in IRS by A19,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,A14,A18,A19,FUNCT_1:70,WELLORD1:37,ZFMISC_1:37;
      then y in (IRS-Seg t)\/{t} & (IRS-Seg t)\/{t} c= IRS-Seg(x)
      by A17,A18,XBOOLE_1:8;
      hence thesis;
    end;
A20: f.x=h.(x,fIx)&fIx in PFuncs(cRS,bX) by A12,PARTFUN1:119,WELLFND1:def 5;
    per cases;
    suppose
A21:  for q be Element of X() st q in union(rng fIx) holds P[x,q];
      then
A22:  f.x=union(rng fIx)\/{x} by A11,A20;
      hence f.x c= IRS-Seg x\/{x} by A15,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 A21;
      assume
A23:  not x in f.x;
      x in {x} by TARSKI:def 1;
      hence thesis by A22,A23,XBOOLE_0:def 2;
    end;
    suppose
A24:  ex q be Element of X() st q in union (rng fIx) & not P[x,q];
      then
A25:  f.x c= IRS-Seg x & IRS-Seg x c= IRS-Seg x\/{x}
      by A11,A15,A20,XBOOLE_1:7;
      hence f.x c= IRS-Seg x\/{x} by XBOOLE_1:1;
      thus thesis by A24,A25,WELLORD1:def 1;
    end;
  end;
A26: for x being Element of RS holds S[x] from WELLFND1:sch 3(A13,A6);
  thus for x,y be Element of X() st x in A & y in A & x <> y holds P[x,y]
  proof
A27: now
      let x be Element of X() such that
A28:  x in A;
      consider y such that
A29:  x in y & y in rng f by A28,TARSKI:def 4;
      consider z be set such that
A30:  z in dom f & f.z=y by A29,FUNCT_1:def 5;
      reconsider z as Element of RS by A30;
      defpred T[set] means x in f.$1;
A31:  T[z] by A29,A30;
      consider p being Element of RS such that
A32:  T[p] and
A33:  not ex q being Element of RS st
      p <> q & T[q] & [q,p] in IRS from WELLFND1:sch 2(A31,A6);
      p = x
      proof
        assume
A34:    p<>x;
        set fIp=f|IRS-Seg p;
A35:    f.p=h.(p,fIp) & fIp in PFuncs(cRS, bX)
        by A12,PARTFUN1:119,WELLFND1:def 5;
        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 A11,A34,A35,TARSKI:def 1;
            hence x in union(rng fIp) by A32,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 A11,A32,A35;
          end;
        end;
        then consider y' be set such that
A36:    x in y' & y' in rng fIp by TARSKI:def 4;
        consider z' be set such that
A37:    z' in dom fIp & fIp.z'=y' by A36,FUNCT_1:def 5;
        reconsider z' as Point of RS by A37;
        z' in IRS-Seg p & f.z'=y' by A37,FUNCT_1:70,RELAT_1:86;
        then z'<> p & [z',p] in IRS & T[z'] by A36,WELLORD1:def 1;
        hence thesis by A33;
      end;
      hence x in f.x by A32;
    end;
A38: now
      let x,y be Element of X() such that
A39:  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 A39,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 A27,A39,FUNCT_1:70,def 5;
      then y in f.y & x in union(rng fIy) by A27,A39,TARSKI:def 4;
      then P[y,x] by A26;
      hence P[x,y] by A1;
    end;
    let x,y be Element of X() such that
A40: 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 A40,RELAT_2:def 6;
    then P[x,y] or P[y,x] by A38,A40;
    hence thesis by A1;
  end;
  let x be Element of X();
  per cases;
  suppose
A41: x in A;
    take y=x;
    thus thesis by A2,A41;
  end;
  suppose
A42: not x in A;
    not x in f.x
    proof
      assume
A43:  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 A42,A43,TARSKI:def 4;
    end;
    then consider r be Element of X() such that
A44: r in union(rng (f|IRS-Seg x)) & not P[x,r] by A26;
    take r;
    union rng (f|IRS-Seg x) c= A by RELAT_1:99,ZFMISC_1:95;
    hence thesis by A44;
  end;
end;

theorem Th30:
  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 Th31:
  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
A10: 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
A11:  x1 in A & x2 in A & F.x1 = F.x2;
      reconsider p1=x1,p2=x2 as Point of M by A11;
      F.x1 in G by A10,A11;
      then consider w be Point of M such that
A12:  F.x1 = Ball(w,r/2) by A6;
      p1 in Ball(w,r/2) & p2 in Ball(w,r/2) by A10,A11,A12;
      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,A11;
    end;
    then F is one-to-one & dom F=A by FUNCT_2:25,def 1;
    then
A13: A,rng F are_equipotent by WELLORD2:def 4;
    rng F c= G
    proof
      let x such that
A14:  x in rng F;
      ex y st y in dom F & x=F.y by A14,FUNCT_1:def 5;
      hence thesis by A10;
    end;
    then rng F is finite by A4;
    hence A is finite by A13,CARD_1:68;
  end;
  assume
A15: 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
A16: r>0;
  consider A be Subset of M such that
A17: for p,q be Point of M st p <> q & p in A & q in A holds dist(p,q) >= r and
A18: for p be Point of M ex q be Point of M st q in A& p in Ball(q,r)
  by A16,Th30;
A19: A is finite by A15,A16,A17;
  deffunc B(Point of M)=Ball($1,r);
  set BA={B(p) where p is Point of M:p in A};
A20: BA is finite from FRAENKEL:sch 21(A19);
  BA c= bool the carrier of M
  proof
    let x such that
A21: x in BA;
    ex p be Point of M st x = B(p) & p in A by A21;
    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
A22:  x in the carrier of M;
      reconsider p=x as Point of M by A22;
      consider q be Point of M such that
A23:  q in A & p in B(q) by A18;
      B(q) in BA by A23;
      hence thesis by A23,TARSKI:def 4;
    end;
    hence thesis by XBOOLE_0:def 10;
  end;
  hence BA is finite & union BA = the carrier of M by A20;
  let C be Subset of M such that
A24: C in BA;
  ex p be Point of M st C=B(p) & p in A by A24;
  hence thesis;
end;

Lm7: 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,METRIC_1:1,PCOMPS_1:33,XREAL_1:217;
  hence x in B & B is open by METRIC_1:12,PRE_TOPC:def 5;
  set VV={ V where V is Subset of T: V in F & V meets B};
  per cases;
  suppose
A4: 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
A5:   v in VV by XBOOLE_0:def 1;
      consider V be Subset of T such that
A6:   v=V & V in F & V meets B by A5;
      consider y be Point of T such that
A7:   V = {y} & y in A by A3,A6;
      reconsider y as Point of M;
      y in B by A6,A7,ZFMISC_1:56;
      then dist(x',y)<r/2 by METRIC_1:12;
      hence thesis by A4,A7;
    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
A8: p in A & dist(p,x') < r/2;
    VV c= {{p}}
    proof
      let v be set such that
A9:   v in VV;
      consider V be Subset of T such that
A10:  v=V & V in F & V meets B by A9;
      consider y be Point of T such that
A11:  V = {y} & y in A by A3,A10;
      reconsider y as Point of M;
      y in B by A10,A11,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 A8,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,A8,A11,TARSKI:def 1;
      hence thesis by A10,A11;
    end;
    hence VV is finite;
  end;
end;

theorem Th32:
  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 Th31;
  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,Lm7;
  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
A7: F is finite by A1,A5,Th27;
  deffunc P(set)=meet $1;
  set PP={P(y) where y is Subset of T:y in F};
A8: PP is finite from FRAENKEL:sch 21(A7);
  A c= PP
  proof
    let y such that
A9: y in A;
    reconsider y'=y as Point of T by A9;
    {y'} in F & {y'} is Subset of T by A9;
    then P({y'}) in PP;
    hence thesis by SETFAM_1:11;
  end;
  hence thesis by A4,A8;
end;

theorem Th33:
  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
A5: for x st x in NAT holds F[x,f.x] from FUNCT_2:sch 1(A2);
A6: dom f=NAT by FUNCT_2:def 1;
  set U = Union f;
A7: U c= the topology of T
  proof
    let x such that
A8: x in U;
    x in union rng f by A8,CARD_3:def 4;
    then consider y such that
A9: x in y & y in rng f by TARSKI:def 4;
    consider z be set such that
A10: z in dom f & f.z=y by A9,FUNCT_1:def 5;
    reconsider z as Element of NAT by A10;
    reconsider X=x as Subset of T by A9;
    consider w be Point of M such that
A11: X=Ball(w,1/(z+1)) by A5,A9,A10;
    thus thesis by A11,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
A12: A is open;
    let p be Point of T such that
A13: p in A;
    reconsider p'=p as Point of M;
    consider r be real number such that
A14: r>0 & Ball(p',r) c= A by A12,A13,TOPMETR:22;
    reconsider r as Real by XREAL_0:def 1;
    consider n be Element of NAT such that
A15: n>0 & 1/n<r/2 by UNIFORM1:2,A14,XREAL_1:217;
    reconsider n1=n-1 as Element of NAT by A15,NAT_1:20;
A16: f.n1 in rng f by A6,FUNCT_1:def 5;
    reconsider fn=f.n1 as Subset-Family of T;
    the carrier of M = union fn by A5;
    then consider x be set such that
A17: p in x & x in fn by TARSKI:def 4;
    reconsider x as Subset of M by A17;
    consider w be Point of M such that
A18: x=Ball(w,1/(n1+1)) by A5,A17;
    reconsider B=Ball(w,1/n) as Subset of T;
    take B;
    B in union rng f by A16,A17,A18,TARSKI:def 4;
    hence B in U & p in B by A17,A18,CARD_3:def 4;
    let q be set such that
A19: q in B;
    reconsider q'=q as Point of M by A19;
    dist(q',w)<1/n & dist(w,p')<1/(n1+1) by A17,A18,A19,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 A15,XREAL_1:10,XXREAL_0:2;
    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 A14;
  end;
  then
A20: U is Basis of T by A7,YELLOW_9:32;
  now
    let x such that
A21: x in dom f;
    reconsider i=x as Element of NAT by A21;
    reconsider fx=f.i as Subset-Family of T;
    fx is finite by A5;
    hence f.x is countable by CARD_4:43;
  end;
  then U is countable by A6,CARD_4:44,61;
  then
A22: Card U c= omega by CARD_4:def 1;
  set CB={Card B where B is Basis of T : not contradiction};
  Card U in CB & weight T = meet CB by A20,WAYBEL23:def 5;
  then weight T c= Card U by SETFAM_1:4;
  then weight T c= omega by A22,XBOOLE_1:1;
  hence thesis by WAYBEL23:def 6;
end;

theorem Th34:
  for T be non empty TopSpace holds T is second-countable implies
  for F being Subset-Family of T st F is Cover of T & F is open
  ex G being Subset-Family of T st G c= F & G is 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 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
A8:   for y st y in F holds not b c= y;
      take E={}T;
      thus thesis by A8;
    end;
  end;
  consider p be Function of B,bool(the carrier of T) such that
A9: for x st x in B holds P[x,p.x] from FUNCT_2:sch 1(A5);
  take RNG=rng p\{{}};
A10: dom p=B by FUNCT_2:def 1;
  thus RNG c= F
  proof
    let y such that
A11: y in RNG;
    y in rng p by A11,XBOOLE_0:def 4;
    then consider z be set such that
A12: z in dom p & p.z=y by FUNCT_1:def 5;
    reconsider z as Subset of T by A10,A12;
    (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 A9,A11,A12,ZFMISC_1:64;
    hence thesis by A12;
  end;
  thus RNG is Cover of T
  proof
    the carrier of T c= union RNG
    proof
      let y such that
A13:  y in the carrier of T;
      reconsider q=y as Point of T by A13;
      consider W be Subset of T such that
A14:  q in W & W in F by A2,PCOMPS_1:5;
      W is open by A3,A14,TOPS_2:def 1;
      then consider U be Subset of T such that
A15:  U in B & q in U & U c= W by A14,YELLOW_9:31;
A16:  p.U in rng p by A10,A15,FUNCT_1:def 5;
      then reconsider pU=p.U as Subset of T;
A17:  pU in F & U c= pU by A9,A14,A15;
      then pU in RNG by A15,A16,ZFMISC_1:64;
      hence thesis by A15,A17,TARSKI:def 4;
    end;
    then [#]T=union RNG by XBOOLE_0:def 10;
    hence thesis by SETFAM_1:60;
  end;
  Card rng p c= Card B & Card B c= omega by A4,A10,CARD_2:80,CARD_4:def 1;
  then Card rng p c= omega by XBOOLE_1:1;
  then rng p is countable by CARD_4:def 1;
  hence thesis by CARD_4:49;
end;

begin :: The main theorem

theorem Th35:
  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 Th20;
  assume
A1: T is countably_compact;
  then M is totally_bounded by Th32;
  then
A2: T is second-countable by Th33;
  let F be Subset-Family of T such that
A3: F is Cover of T & F is open;
  consider G be Subset-Family of T such that
A4: G c= F & G is Cover of T & G is countable by A2,A3,Th34;
  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 Cover of T & H is finite by A1,A4,Def9;
  thus thesis by A4,A5,XBOOLE_1:1;
end;

theorem Th36:
  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 c= 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
A7: for x st x in A holds P[x,p.x] from FUNCT_2:sch 1(A4);
  consider x such that
A8: x in A by A2,XBOOLE_0:def 1;
  consider y such that
A9: y in I & P[x,y] by A4,A8;
  dom p=A & rng p is finite by A3,A9,FUNCT_2:def 1;
  then consider t be set such that
A10: t in rng p & p"{t} is infinite by A2,Th24;
  consider Y,Z be set such that
A11: Y in F & Z in {A} & t=Y/\Z by A10,SETFAM_1:def 5;
  reconsider Y as Subset of X by A11;
  take Y;
A12: Z = A by A11,TARSKI:def 1;
  p"{t} c= Y/\A
  proof
    let z be set such that
A13: z in p"{t};
    z in dom p & p.z in {t} by A13,FUNCT_1:def 13;
    then z in A & p.z=t by TARSKI:def 1;
    hence thesis by A7,A11,A12;
  end;
  hence thesis by A10,A11;
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,Th36;
    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
A10: CXA in bool cM & Q[CXA] by A7,A8,Th6,Th8;
A11: 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
A12:  x in bool cM & Q[x];
      reconsider X=x as Subset of M by A12;
      reconsider X'=X as Subset of T;
      set d=diameter X;
      per cases by A12,TBSP_1:29;
      suppose
A14:    d=0;
        take Y=X;
        thus thesis by A12,A14;
      end;
      suppose d>0;
        then
A15:    d/4>0 by XREAL_1:226;
        then consider F be Subset-Family of M such that
A16:    F is finite and
A17:    cM = union F and
A18:    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 A12;
        then consider Y be Subset of M such that
A19:    Y in F & Y /\ X is infinite by A16,A17,Th36;
        set YX=Y/\X;
        consider w be Point of M such that
A20:    Y = Ball(w,d/4) by A18,A19;
        Y is bounded & YX c= Y by A20,TBSP_1:19,XBOOLE_1:17;
        then
A21:    YX is bounded & diameter YX <=diameter Y & diameter Y<=2*( d /4)
        by A15,A20,TBSP_1:21,31,32;
        then
A22:    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;
A23:    yx c= Cl yx by PRE_TOPC:48;
        X is closed by A12;
        then X' is closed & yx c= X' by Th6,XBOOLE_1:17;
        hence thesis by A19,A21,A22,A23,Th6,Th8,TOPS_1:31;
      end;
    end;
    consider f be Function such that
A24: dom f = NAT & rng f c= bool cM and
A25: f.0 = CXA and
A26: for k be Element of NAT
    holds P[f.k,f.(k+1)] & Q[f.k] from TREES_2:sch 5(A10,A11);
    reconsider f as SetSequence of M by A24,FUNCT_2:4;
A27: now
      let x such that
A28:  x in dom f;
      reconsider i=x as Element of NAT by A28;
      f.i is infinite by A26;
      hence f.x is non empty;
    end;
A29: now
      let n;
      n in NAT by ORDINAL1:def 13;
      hence f.n is bounded by A26;
    end;
    now
      let n;
      n in NAT by ORDINAL1:def 13;
      hence f.n is closed by A26;
    end;
    then reconsider f as non-empty bounded closed SetSequence of M
    by A27,A29,Def1,Def8,FUNCT_1:def 15;
    for n be Element of NAT holds f.(n+1) c= f.n by A26;
    then
A30: f is descending by KURATO_2:def 5;
    deffunc F(Element of NAT)=1/(1+$1);
    consider seq be Real_Sequence such that
A31: 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 A31;
    then
A32: seq is convergent & lim seq=0 by SEQ_4:45;
    then
A33: 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,Th8;
    then 0<=diameter CXA & diameter CXA <= 1&seq.0=1/(1+0)&Ns.0=NULL*seq.0
    by A8,A31,Th8,SEQ_1:13,TBSP_1:29;
    then
A34: N[0] by A25,Def2;
A35: for n be Element of NAT st N[n] holds N[n+1]
    proof
      let n be Element of NAT such that
A36:  N[n];
      set n1=n+1;
      df.n<=F(n) & diameter (f.n1)<=(diameter (f.n))/2& diameter (f.n)=df. n
      by A26,A31,A36,Def2;
      then (df.n)/2<=F(n)/2 & df.n1<=(df.n)/2 by Def2,XREAL_1:74;
      then
A37:  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 XCMPLX_1:79,XREAL_1:120;
      then
A38:  F(n1)>=df.n1 by A37,XXREAL_0:2;
      f.n1 is bounded by Def1;
      then 0<= diameter (f.n1) & Ns.n1=NULL*seq.n1 by SEQ_1:13,TBSP_1:29;
      hence thesis by A31,A38,Def2;
    end;
A39: for n be Element of NAT holds N[n] from NAT_1:sch 1(A34,A35);
    then
A40: lim df = 0 & df is convergent by A32,A33,SEQ_2:33,34;
    then meet f is non empty by A2,A30,Th10;
    then consider p be set such that
A41: p in meet f by XBOOLE_0:def 1;
    reconsider p as Point of T by A41;
    reconsider p'=p as Point of M;
    now
      let U be open Subset of T such that
A42:  p in U;
      consider r be real number such that
A43:  r>0 & Ball(p',r) c= U by A42,TOPMETR:22;
      r/2 >0 by A43,XREAL_1:217;
      then consider n be Element of NAT such that
A44:  for m be Element of NAT st n<=m holds abs(df.m-0)<r/2
      by A40,SEQ_2:def 7;
      f.n is infinite by A26;
      then Card {p} in Card (f.n) & p in f.n by A41,CARD_FIL:1,KURATO_2:6;
      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
A45:  q in f.n\{p} by XBOOLE_0:def 1;
      reconsider q as Point of T by A45;
      reconsider q'=q as Point of M;
      reconsider B=Ball(q',dist(p',q')) as Subset of T;
      q<>p by A45,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 METRIC_1:1,2,5,PCOMPS_1:33;
      then B is open & q in B & f.n c= Cl xa & q in f.n
      by A25,A30,A45,KURATO_2:22,METRIC_1:12,PRE_TOPC:def 5,ZFMISC_1:64;
      then B meets xa by PRE_TOPC:54;
      then consider s be set such that
A46:  s in B & s in xa by XBOOLE_0:3;
      reconsider s as Point of M by A46;
      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 A39,A44,SEQ_1:13;
      then df.n<r/2 & p in f.n & q in f.n & f.n is bounded
      by A26,A41,A45,ABSVALUE:def 1,KURATO_2:6,ZFMISC_1:64;
      then dist(p',q')<=diameter (f.n) & diameter (f.n) < r/2
      by Def2,TBSP_1:def 10;
      then
A47:  dist(p',q')<r/2&dist(q',s)<dist(p',q') by A46,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 A47,METRIC_1:4,XREAL_1:10;
      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 A43,A46,XBOOLE_0:def 3;
      hence s' in A/\U & s'<>p by A46,METRIC_1:12,XBOOLE_0:def 3;
    end;
    hence Der A is non empty by TOPGEN_1:19;
  end;
  then T is countably_compact by Th28;
  hence thesis by Th35;
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 Th38:
  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
A3: x=[y,b] & (y in X & b<>a or y = X & b = a);
  per cases by A3;
  suppose
A4: 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 A4;
    end;
    then b in (the carrier of M)\{a} by A4,ZFMISC_1:64;
    then x in [:X,(the carrier of M)\{a}:] by A3,A4,ZFMISC_1:106;
    hence thesis by XBOOLE_0:def 2;
  end;
  suppose y = X & b = a;
    then x in {[X,a]} by A3,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,Th38;
      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,Th38;
      now per cases;
        suppose
A5:       x1 = y1;
          take d=dist(x2,y2);
          thus d in REAL;
          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
A8:       x1<>y1;
          take d=dist(x2,a)+dist(a,y2);
          thus d in REAL;
          let x',y' be Element of XX such that
A9:       x'=x & y'=y;
          let x1',y1' be set, x2',y2' be Point of M such that
A10:      x' = [x1',x2'] & y' = [y1',y2'];
          x1'=x1 & x2'=x2 & y1'=y1 & y2'=y2 by A3,A4,A9,A10,ZFMISC_1:33;
          hence (x1' = y1' implies d = dist(x2',y2') ) &
          (x1' <> y1' implies d = dist(x2',a)+dist(a,y2')) by A8;
        end;
      end;
      hence thesis;
    end;
    consider f being Function of [:XX,XX:],REAL such that
A11: 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 A11;
  end;
  uniqueness
  proof
    set XX=[:X,(the carrier of M)\{a}:]\/{[X,a]};
    let w1,w2 be Function of [:XX,XX:],REAL such that
A12: 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
A13: 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
A14:  x in XX & y in XX;
      consider x1 be set,x2 be Point of M such that
A15:  x=[x1,x2] & (x1 in X & x2<>a or x1 = X & x2 = a) by A14,Th38;
      consider y1 be set,y2 be Point of M such that
A16:  y=[y1,y2] & (y1 in X & y2<>a or y1 = X & y2 = a) by A14,Th38;
      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 A12,A13,A14,A15,A16;
      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
A1: 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
A2: 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 Th38;
          hence dist(a,a) = w.([X,a],[X,a]) by Def10
            .= 0 by A3,A4,METRIC_1:def 3;
        end;
        suppose a<>A;
          then
A5:       [x0,a] in XX by A1,Th38;
          hence dist(a,a) = w.([x0,a],[x0,a]) by Def10
            .= 0 by A3,A5,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
A6: 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
A7:       a=A & b<>A;
          then
A8:       [X,A] in XX & [x0,b] in XX by A1,Th38;
A9:       X<>x0 by A1;
          then dist(A,A)+dist(A,b) = w.([X,A],[x0,b]) by A8,Def10
            .= w.([x0,b],[X,A]) by A6,A8,METRIC_1:def 5
            .= dist(b,A)+dist(A,A) by A8,A9,Def10;
          hence dist(a,b)=dist(b,a) by A7;
        end;
        suppose
A10:      a<>A & b=A;
          then
A11:      [X,A] in XX & [x0,a] in XX by A1,Th38;
A12:      X<>x0 by A1;
          then dist(A,A)+dist(A,a) = w.([X,A],[x0,a]) by A11,Def10
            .= w.([x0,a],[X,A]) by A6,A11,METRIC_1:def 5
            .= dist(a,A)+dist(A,A) by A11,A12,Def10;
          hence dist(a,b)=dist(b,a) by A10;
        end;
        suppose a<>A & b<>A;
          then
A13:      [x0,a] in XX & [x0,b] in XX by A1,Th38;
          hence dist(a,b) = w.([x0,a],[x0,b]) by Def10
            .= w.([x0,b],[x0,a]) by A6,A13,METRIC_1:def 5
            .= dist(b,a) by A13,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
A14: 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 Th38;
          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 A14,Def10,METRIC_1:def 6;
          hence dist(a,c)<=dist(a,b)+dist(b,c);
        end;
        suppose
A15:      a=A & b=A & c <> A;
          then reconsider Xa=[X,a],Xb=[X,b],Xc =[x0,c] as Element of XX
          by A1,Th38;
          x0<>X by A1;
          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 A2,A14,A15,Def10,METRIC_1:1,def 6;
          hence dist(a,c)<=dist(a,b)+dist(b,c);
        end;
        suppose
A16:      a=A & b<>A & c = A;
          then reconsider Xa=[X,a],Xb=[x0,b],Xc =[X,c] as Element of XX
          by A1,Th38;
          x0<>X by A1;
          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 A2,A14,A16,Def10,METRIC_1:1,def 6;
          hence dist(a,c)<=dist(a,b)+dist(b,c);
        end;
        suppose
A17:      a=A & b<>A & c <> A;
          then reconsider Xa=[X,a],Xb=[x0,b],Xc =[x0,c] as Element of XX
          by A1,Th38;
          x0<>X by A1;
          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 A2,A14,A17,Def10,METRIC_1:1,def 6;
          hence dist(a,c)<=dist(a,b)+dist(b,c);
        end;
        suppose
A18:      a<>A & b=A & c =A;
          then reconsider Xa=[x0,a],Xb=[X,b],Xc =[X,c] as Element of XX
          by A1,Th38;
          x0<>X by A1;
          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 A2,A14,A18,Def10,METRIC_1:1,def 6;
          hence dist(a,c)<=dist(a,b)+dist(b,c);
        end;
        suppose
A19:      a<>A & b=A & c <>A;
          then reconsider Xa=[x0,a],Xb=[X,b],Xc =[x0,c] as Element of XX
          by A1,Th38;
          x0<>X by A1;
          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 A2,A14,A19,Def10,METRIC_1:1,def 6;
          hence dist(a,c)<=dist(a,b)+dist(b,c);
        end;
        suppose
A20:      a<>A & b<>A & c = A;
          then reconsider Xa=[x0,a],Xb=[x0,b],Xc =[X,c] as Element of XX
          by A1,Th38;
          x0<>X by A1;
          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 A2,A14,A20,Def10,METRIC_1:1,def 6;
          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 A1,Th38;
          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 A14,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
A21: w is discerning Reflexive;
  now
    let a,b be Point of M;
    assume
A22: dist(a,b)=0;
    now per cases;
      suppose a=A & b=A;
        hence a=b;
      end;
      suppose
A23:    a=A & b<>A;
        then reconsider Xa=[X,a],Xb=[x0,b] as Element of XX by A1,Th38;
        x0<>X by A1;
        then dist(a,a)+dist(a,b)=w.(Xa,Xb) & dist(a,a)=0
        by A2,A21,A23,Def10,METRIC_1:1;
        then Xa=Xb by A21,A22,METRIC_1:def 4;
        hence a=b by ZFMISC_1:33;
      end;
      suppose
A24:    a<>A & b=A;
        then reconsider Xa=[x0,a],Xb=[X,b] as Element of XX by A1,Th38;
        x0<>X by A1;
        then dist(a,b)+dist(b,b)=w.(Xa,Xb) & dist(b,b)=0
        by A2,A21,A24,Def10,METRIC_1:1;
        then Xa=Xb by A21,A22,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 A1,Th38;
        dist(a,b)=w.(Xa,Xb) by Def10;
        then Xa=Xb by A21,A22,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;

Lm8: 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 Th38;
      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
A3: M is symmetric;
    now
      let A,B be Element of XX;
      consider y1 be set,b1 be Point of M such that
A4:   A=[y1,b1] & (y1 in X & b1<>a or y1 = X & b1 = a) by Th38;
      consider y2 be set,b2 be Point of M such that
A5:   B=[y2,b2] & (y2 in X & b2<>a or y2 = X & b2 = a) by Th38;
      now per cases by A4,A5;
        suppose b1=a & y1=X & b2=a & y2=X;
          hence w.(A,B)=w.(B,A) by A4,A5;
        end;
        suppose
A6:       y1 <>y2;
          hence w.(A,B) = dist(b1,a)+dist(a,b2) by A4,A5,Def10
            .= dist(a,b1)+dist(a,b2) by A3,METRIC_1:3
            .= dist(a,b1)+dist(b2,a) by A3,METRIC_1:3
            .= w.(B,A) by A4,A5,A6,Def10;
        end;
        suppose
A7:       b1<>a & b2<>a & y1=y2;
          hence w.(A,B) = dist(b1,b2) by A4,A5,Def10
            .= dist(b2,b1) by A3,METRIC_1:3
            .=w.(B,A) by A4,A5,A7,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
A8: 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
A9:   A=[y1,b1] & (y1 in X & b1<>a or y1 = X & b1 = a) by Th38;
      consider y2 be set,b2 be Point of M such that
A10:  B=[y2,b2] & (y2 in X & b2<>a or y2 = X & b2 = a) by Th38;
      consider y3 be set,b3 be Point of M such that
A11:  C=[y3,b3] & (y3 in X & b3<>a or y3 = X & b3 = a) by Th38;
      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 A8,A9,A10,A11,Def10,METRIC_1:4;
          hence w.(A,C)<=w.(A,B)+w.(B,C);
        end;
        suppose y1<>y2 & y1=y3;
          then
A12:      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 A8,A9,A10,A11,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 A8,METRIC_1:4,XREAL_1:9;
          hence w.(A,C)<=w.(A,B)+w.(B,C) by A12,XXREAL_0:2;
        end;
        suppose y1=y2 & y1<>y3;
          then
A13:      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 A8,A9,A10,A11,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 A13;
        end;
        suppose y1<>y2 & y1<>y3 & y2<>y3;
          then
A14:      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 A9,A10,A11,Def10;
          0<=dist(a,b2) & 0<=dist(b2,a) by A8,METRIC_1:5;
          then dist(b1,a)+0<=w.(A,B)&0+dist(a,b3)<=w.(B,C) by A14,XREAL_1:8;
          hence w.(A,C)<=w.(A,B)+w.(B,C) by A14,XREAL_1:9;
        end;
        suppose y1<>y2 & y1<>y3 & y2=y3;
          then
A15:      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 A8,A9,A10,A11,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 A15;
        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
A16: M is triangle symmetric Reflexive discerning;
  now
    let A,B be Element of XX;
    assume
A17: w.(A,B)=0;
    consider y1 be set,b1 be Point of M such that
A18: A=[y1,b1] & (y1 in X & b1<>a or y1 = X & b1 = a) by Th38;
    consider y2 be set,b2 be Point of M such that
A19: B=[y2,b2] & (y2 in X & b2<>a or y2 = X & b2 = a) by Th38;
    now per cases;
      suppose
A20:    y1=y2;
        then w.(A,B)=dist(b1,b2) by A18,A19,Def10;
        hence A=B by A16,A17,A18,A19,A20,METRIC_1:2;
      end;
      suppose y1<>y2;
        then w.(A,B)=dist(b1,a)+dist(a,b2) & dist(a,b2)>=0 & dist(b1,a)>=0
        by A16,A18,A19,Def10,METRIC_1:5;
        then dist(b1,a)=0 & dist(a,b2)=0 by A17;
        hence A=B by A16,A18,A19,METRIC_1:2;
      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 Lm8;
end;

registration
  let M be symmetric MetrStruct;
  let a be Point of M;
  let X be set;
  cluster WellSpace(a,X) -> symmetric;
  coherence by Lm8;
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 Lm8;
end;

registration
  let M be MetrSpace;
  let a be Point of M;
  let X be set;
  cluster WellSpace(a,X) -> discerning;
  coherence by Lm8;
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
A1: x0 in X by XBOOLE_0:def 1;
  assume
A2: WellSpace(a,X) is complete;
  set W=WellSpace(a,X);
  let S be sequence of M such that
A3: S is Cauchy;
  defpred P[set,set] means
  (S.$1<>a implies $2=[x0,S.$1]) & (S.$1=a implies $2=[X,S.$1]);
A4: for x st x in NAT ex y st y in the carrier of W & P[x,y]
  proof
    let x such that
A5: x in NAT;
    reconsider i=x as Element of NAT by A5;
    per cases;
    suppose
A6:   S.i<>a;
      take xS=[x0,S.i];
      thus thesis by A1,A6,Th38;
    end;
    suppose
A7:   S.x=a;
      take xS=[X,a];
      thus thesis by A7,Th38;
    end;
  end;
  consider S' be sequence of W such that
A8: for x st x in NAT holds P[x,S'.x] from FUNCT_2:sch 1(A4);
  S' is Cauchy
  proof
    let r such that
A9: r>0;
    consider p be Element of NAT such that
A10: for n,m be Element of NAT st p<=n & p<=m holds dist(S.n,S.m)<r
    by A3,A9,TBSP_1:def 5;
    take p;
    let n,m be Element of NAT such that
A11: 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 A8;
      then dist(S'.n,S'.m)=dist(S.n,S.m) by Def10;
      hence thesis by A10,A11;
    end;
    suppose
A12:  S.n<>a & S.m=a;
      then [x0,S.n]=S'.n & [X,S.m]=S'.m & X<>x0 by A1,A8;
      then dist(S'.n,S'.m)=dist(S.n,S.m)+dist(S.m,S.m) & dist(S.m,S.m)=0
      by A12,Def10,METRIC_1:1;
      hence thesis by A10,A11;
    end;
    suppose
A13:  S.n=a & S.m<>a;
      then [X,S.n]=S'.n & [x0,S.m]=S'.m & X<>x0 by A1,A8;
      then dist(S'.n,S'.m)=dist(S.n,S.n)+dist(S.n,S.m) & dist(S.n,S.n)=0
      by A13,Def10,METRIC_1:1;
      hence thesis by A10,A11;
    end;
    suppose S.n<>a & S.m<>a;
      then [x0,S.n]=S'.n & [x0,S.m]=S'.m by A8;
      then dist(S'.n,S'.m)=dist(S.n,S.m) by Def10;
      hence thesis by A10,A11;
    end;
  end;
  then S' is convergent by A2,TBSP_1:def 6;
  then consider L being Element of W such that
A14: 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
A15: L=[L1,L2] & (L1 in X & L2<>a or L1 = X & L2 = a) by Th38;
  take L2;
  let r such that
A16: r>0;
  consider n be Element of NAT such that
A17: for m be Element of NAT st n<=m holds dist(S'.m,L)<r by A14,A16;
  take n;
  let m be Element of NAT such that
A18: n<=m;
  per cases;
  suppose
A19: S.m=a & L1=X;
    then S'.m=[X,a] by A8;
    then dist(S'.m,L)=dist(S.m,L2) by A15,A19,Def10;
    hence thesis by A17,A18;
  end;
  suppose
A20: S.m=a & L1<>X;
    then S'.m=[X,a] by A8;
    then dist(S'.m,L)=dist(S.m,S.m)+dist(S.m,L2) & dist(S.m,S.m)=0
    by A15,A20,Def10,METRIC_1:1;
    hence thesis by A17,A18;
  end;
  suppose
A21: S.m <> a & L1=x0;
    then S'.m=[x0,S.m] by A8;
    then dist(S'.m,L)=dist(S.m,L2) by A15,A21,Def10;
    hence thesis by A17,A18;
  end;
  suppose
A22: S.m <> a & L1<>x0;
    then S'.m=[x0,S.m] by A8;
    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 A15,A17,A18,A22,Def10,METRIC_1:4;
    hence thesis by XXREAL_0:2;
  end;
end;

theorem Th41:
  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);
  let S be sequence of W such that
A1: S is Cauchy;
  reconsider Xa=[X,a] as Point of W by Th38;
  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
A2: r > 0 and
A3: for n ex m st m >= n & dist(S.m,Xa) >= r;
    consider p be Element of NAT such that
A4: for n,m be Element of NAT st n>=p & m>=p holds dist(S.n,S.m)<r
    by A1,A2,TBSP_1:def 5;
    consider p' be natural number such that
A5: p' >= p & dist(S.p',Xa) >= r by A3;
    consider Y be set,y be Point of M such that
A6: S.p'=[Y,y] & (Y in X & y<>a or Y = X & y = a) by Th38;
    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
A7:   m >= p';
      consider Z be set,z be Point of M such that
A8:   S.m=[Z,z] & (Z in X & z<>a or Z = X & z = a) by Th38;
      Y = Z
      proof
        assume
A9:     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 A6,Def10;
        then dist(y,a)>=r & dist(a,z) >=0 by A5,METRIC_1:5;
        then dist(y,a)+dist(a,z)>=r+0 & m>=p & m in NAT & p' in NAT
        by A5,A7,ORDINAL1:def 13,XREAL_1:9,XXREAL_0:2;
        then dist(S.p',S.m)>=r &dist(S.p',S.m)<r by A4,A5,A6,A8,A9,Def10;
        hence thesis;
      end;
      hence thesis by A8;
    end;
    hence thesis;
  end;
end;

theorem Th42:
  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);
  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 Th38;
    take s2;
    thus thesis by A5;
  end;
  consider S be sequence of M such that
A6: 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
A7: r>0;
    consider p be Element of NAT such that
A8: for n,m be Element of NAT st p<=n & p<=m holds dist(S'.n,S'.m)<r
    by A2,A7,TBSP_1:def 5;
    take p;
    let n,m be Element of NAT such that
A9: p<=n & p<=m;
    consider x such that
A10: S'.n=[x,S.n] by A6;
    consider y such that
A11: S'.m=[y,S.m] by A6;
    per cases;
    suppose x=y;
      then dist(S'.n,S'.m)=dist(S.n,S.m) by A10,A11,Def10;
      hence thesis by A8,A9;