:: Brouwer Fixed Point Theorem for Simplexes
::  by Karol P\kak
::
:: Received December 21, 2010
:: Copyright (c) 2010-2012 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies ABIAN, AOFA_I00, ARYTM_1, ARYTM_3, CARD_1, CARD_3, CLASSES1,
      COMPLEX1, CONVEX1, EUCLID, EUCLID_9, FINSEQ_1, FINSEQ_2, FINSEQ_4,
      FINSET_1, FUNCOP_1, FUNCT_1, FUNCT_2, FUNCT_4, GLIB_000, INT_1, MATROID0,
      MEASURE5, MEMBERED, METRIC_1, NAT_1, NEWTON, NUMBERS, ORDERS_1, ORDINAL1,
      ORDINAL2, ORDINAL4, PARTFUN1, PCOMPS_1, PEPIN, POWER, PRE_TOPC, QC_LANG1,
      RCOMP_1, REAL_1, RELAT_1, RLAFFIN1, RLAFFIN2, RLVECT_1, RLVECT_2,
      RLVECT_5, RUSUB_4, SEMI_AF1, SEQ_4, SETFAM_1, SGRAPH1, SIMPLEX0,
      SIMPLEX1, SQUARE_1, STRUCT_0, SUBSET_1, SUPINF_2, TARSKI, TOPDIM_1,
      TOPMETR, TOPS_1, TOPS_2, VALUED_1, WEIERSTR, XBOOLE_0, XREAL_0, XXREAL_0,
      XXREAL_1, XXREAL_2, ZFMISC_1, SIMPLEX2;
 notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, ZFMISC_1, RELAT_1, FUNCT_1,
      RELSET_1, FUNCT_2, PARTFUN1, FUNCOP_1, FUNCT_4, XXREAL_3, VALUED_1,
      PRE_TOPC, NUMBERS, XREAL_0, FINSEQ_1, BINOP_1, FINSEQ_2, TOPMETR,
      METRIC_1, EUCLID, FINSET_1, XXREAL_0, REAL_1, SETFAM_1, TOPS_2, INT_1,
      STRUCT_0, COMPTS_1, PCOMPS_1, RCOMP_1, WEIERSTR, SEQ_4, XXREAL_2,
      RVSUM_1, RLVECT_1, RUSUB_4, RLVECT_5, SIMPLEX0, RLAFFIN1, RLAFFIN2,
      SIMPLEX1, ORDERS_1, CARD_1, DOMAIN_1, PENCIL_1, CLASSES1, RLTOPSP1,
      MATROID0, TBSP_1, MEMBERED, RLVECT_2, CONVEX1, TOPREAL9, COMPLEX1,
      NEWTON, POWER, SQUARE_1, BORSUK_1, CARD_3, EUCLID_9, TMAP_1, FINSEQOP,
      ABIAN, TOPDIM_1, TOPDIM_2, RLAFFIN3;
 constructors ABIAN, BINOP_2, COMPTS_1, CONVEX1, EUCLID_9, FINSEQOP, FUNCSDOM,
      MONOID_0, NEWTON, POWER, REAL_1, RFINSEQ2, RLAFFIN1, RLAFFIN2, RLAFFIN3,
      RLVECT_5, RUSUB_5, SEQ_1, SEQ_4, SIMPLEX1, SQUARE_1, TBSP_1, TMAP_1,
      TOPDIM_1, TOPDIM_2, TOPREAL9, TOPS_2, WAYBEL23, WEIERSTR;
 registrations ASYMPT_0, BORSUK_1, BORSUK_2, CARD_1, COMPTS_1, EUCLID,
      EUCLID_9, FINSEQ_1, FINSEQ_2, FINSET_1, FUNCT_1, FUNCT_2, INT_1,
      JORDAN2B, JORDAN2C, MEMBERED, METRIZTS, MONOID_0, NAT_1, NEWTON, NUMBERS,
      PCOMPS_1, PRE_TOPC, RELAT_1, RELSET_1, RLAFFIN1, RLAFFIN3, SEQ_4,
      SIMPLEX0, SIMPLEX1, STRUCT_0, SUBSET_1, TBSP_1, TMAP_1, TOPDIM_1,
      TOPDIM_2, TOPMETR, TOPREAL9, TOPREALC, TOPS_1, VALUED_0, VALUED_1,
      XBOOLE_0, XREAL_0, XXREAL_0, XXREAL_2, XXREAL_3, YELLOW13, JORDAN,
      ORDINAL1;
 requirements REAL, SUBSET, NUMERALS, ARITHM, BOOLE;
 definitions EUCLID, METRIC_1, ORDINAL1, PCOMPS_1, RLVECT_1, SIMPLEX0,
      SIMPLEX1, STRUCT_0, SUBSET_1, TARSKI, TBSP_1, XCMPLX_0;
 theorems ABIAN, ABSVALUE, BINOP_1, BORSUK_1, BORSUK_3, BORSUK_5, CARD_1,
      CARD_2, CLASSES1, COMPTS_1, CONVEX1, EUCLID, EUCLID_9, FINSEQ_1,
      FINSEQ_2, FINSEQ_3, FINSEQ_4, FUNCOP_1, FUNCT_1, FUNCT_2, FUNCT_4,
      HAUSDORF, INT_1, JORDAN1K, JORDAN2B, JORDAN2C, MATROID0, MEMBERED,
      METRIC_1, NAT_1, NEWTON, ORDERS_1, ORDINAL1, PARTFUN1, PCOMPS_1,
      PCOMPS_2, POWER, PRE_TOPC, RCOMP_1, RELAT_1, RLAFFIN1, RLAFFIN2,
      RLAFFIN3, RLVECT_1, RLVECT_2, RLVECT_3, RUSUB_4, RVSUM_1, SETFAM_1,
      SIMPLEX0, SIMPLEX1, TARSKI, TBSP_1, TMAP_1, TOPDIM_1, TOPDIM_2, TOPGEN_5,
      TOPGRP_1, TOPMETR, TOPREAL3, TOPREAL6, TOPREAL7, TOPREAL9, TOPREALC,
      TOPS_1, TOPS_2, TOPS_3, TSEP_1, VALUED_1, WEIERSTR, XBOOLE_0, XBOOLE_1,
      XCMPLX_1, XREAL_0, XREAL_1, XXREAL_0, XXREAL_1, XXREAL_2, XXREAL_3,
      ZFMISC_1, JORDAN5A;
 schemes FINSEQ_1, FRAENKEL, FUNCT_2, NAT_1, NAT_2, SUBSET_1;

begin :: The Lebesgue Number

reserve M for non empty MetrSpace,
        F,G for open Subset-Family of TopSpaceMetr M;

definition
  let M such that
    B1: TopSpaceMetr M is compact;
  let F be Subset-Family of TopSpaceMetr M such that
    B2: F is open and
    B3: F is Cover of TopSpaceMetr M;
   mode Lebesgue_number of F -> positive Real means :Def1:
     for p be Point of M
     ex A be Subset of TopSpaceMetr M st A in F & Ball(p,it) c= A;
  existence
 proof
  set TM=TopSpaceMetr M;
  consider G be Subset-Family of TM such that
   A1: G c=F and
   A2: G is Cover of TM and
   A3: G is finite by B1,B2,B3,COMPTS_1:def 1;
  per cases;
  suppose A4: [#]TM in G;
   take R=1;
   let x be Point of M;
   take[#]TM;
   thus thesis by A1,A4;
  end;
  suppose A5: not[#]TM in G;
   set cTM=[#]TM;
   set FUNCS=Funcs([#]TM,REAL);
   consider g be FinSequence such that
    A6: rng g=G and
    g is one-to-one by A3,FINSEQ_4:58;
   defpred P[Nat,set,set] means
    for f1,f2 be Function of TM,R^1 st f1=$2 & f2=$3 & f1 is continuous holds
f2 is continuous & ex A be non empty Subset of TM st A`=g.($1+1) & for x be
Point of TM holds f2.x=max(f1.x,(dist_min A).x);
   union G is non empty by A2,SETFAM_1:45;
   then A7: g is non empty by A6,ZFMISC_1:2;
   then A8: len g>=1 by NAT_1:14;
   then A9: 1 in dom g by FINSEQ_3:25;
   then A10: g.1 in rng g by FUNCT_1:def 3;
   then reconsider g1=g.1 as Subset of TM by A6;
   A11: g1``<>[#]TM by A5,A6,A9,FUNCT_1:def 3;
   g1 is open by B2,A1,A6,A10,TOPS_2:def 1;
   then reconsider g19=g1` as non empty closed Subset of TM by A11;
   reconsider Dg19=dist_min g19 as Element of FUNCS by FUNCT_2:8,TOPMETR:17;
   A12: for n be Nat st 1<=n & n<len g for x be Element of FUNCS ex y be
Element of FUNCS st P[n,x,y]
   proof
    let n be Nat such that
     1<=n and
     A13: n<len g;
    let x be Element of FUNCS;
    reconsider fx=x as Function of TM,R^1 by TOPMETR:17;
    per cases;
    suppose A14: not fx is continuous;
     take y=x;
     thus thesis by A14;
    end;
    suppose A15: fx is continuous;
     1<=n+1 & n+1<=len g by A13,NAT_1:11,13;
     then A16: n+1 in dom g by FINSEQ_3:25;
     then g.(n+1) in G by A6,FUNCT_1:def 3;
     then reconsider A=g.(n+1) as Subset of TM;
     A``<>[#]TM by A5,A6,A16,FUNCT_1:def 3;
     then reconsider A9=A` as non empty Subset of TM;
     R^1 is SubSpace of R^1 by TSEP_1:2;
     then consider h be continuous Function of TM,R^1 such that
      A17: for x be Point of TM holds h.x=max(fx.x,(dist_min A9).x) by A15,
TOPGEN_5:50;
     reconsider y=h as Element of FUNCS by FUNCT_2:8,TOPMETR:17;
     take y;
     let f1,f2 be Function of TM,R^1 such that
      A18: f1=x and
      A19: f2=y and
      f1 is continuous;
     thus f2 is continuous by A19;
     take A9;
     thus thesis by A17,A18,A19;
    end;
   end;
   consider p be FinSequence of FUNCS such that
    A20: len p=len g and
    A21: p/.1=Dg19 or len g=0 and
    A22: for n be Nat st 1<=n & n<len g holds P[n,p/.n,p/.(n+1)] from NAT_2:sch
1(A12);
   A23: len p in dom p by A8,A20,FINSEQ_3:25;
   p/.(len p) is Element of FUNCS;
   then reconsider pL=p/.(len p) as Function of TM,R^1 by TOPMETR:17;
   reconsider rngPL=rng pL as Subset of R^1 by RELAT_1:def 19;
   set cRpL=[#]rngPL;
   A24: cRpL=rng pL by WEIERSTR:def 1;
   A25: dom p=dom g by A20,FINSEQ_3:29;
   defpred Q[Nat] means
    for f be Function of TM,R^1 st$1 in dom p & f=p/.$1 holds f is continuous &
for j be Nat,h be Function of TM,R^1 st j<=$1 & j in dom p & h=p/.j for x be
Point of TM holds h.x<=f.x;
   A26: for n be Nat st Q[n] holds Q[n+1]
   proof
    let n be Nat;
    assume A27: Q[n];
    let f be Function of TM,R^1 such that
     A28: n+1 in dom p and
     A29: f=p/.(n+1);
    per cases;
    suppose A30: n=0;
     hence f is continuous by A7,A21,A29;
     let j be Nat,g be Function of TM,R^1;
     assume that
      A31: j<=n+1 and
      A32: j in dom p and
      A33: g=p/.j;
     1<=j by A32,FINSEQ_3:25;
     hence thesis by A29,A30,A31,A33,XXREAL_0:1;
    end;
    suppose n>0;
     then reconsider n1=n-1 as Element of NAT by NAT_1:20;
     p/.n is Element of FUNCS;
     then reconsider pn=p/.n as Function of TM,R^1 by TOPMETR:17;
     n+1<=len p by A28,FINSEQ_3:25;
     then A34: 1<=n1+1 & n<len p by NAT_1:11,13;
     then A35: n in dom p by FINSEQ_3:25;
     then A36: pn is continuous by A27;
     hence f is continuous by A20,A22,A29,A34;
     consider A be non empty Subset of TM such that
      A`=g.(n+1) and
      A37: for y be Point of TM holds f.y=max(pn.y,(dist_min A).y) by A20,A22
,A29,A34,A36;
     let j be Nat,h be Function of TM,R^1 such that
      A38: j<=n+1 and
      A39: j in dom p and
      A40: h=p/.j;
     let x be Point of TM;
     A41: f.x=max(pn.x,(dist_min A).x) by A37;
     per cases by A38,NAT_1:8;
     suppose A42: j<=n;
      A43: pn.x<=f.x by A41,XXREAL_0:25;
      h.x<=pn.x by A27,A35,A39,A40,A42;
      hence thesis by A43,XXREAL_0:2;
     end;
     suppose j=n+1;
      hence thesis by A29,A40;
     end;
    end;
   end;
   A44: Q[0] by FINSEQ_3:25;
   A45: for n be Nat holds Q[n] from NAT_1:sch 2(A44,A26);
   A46: dom pL=cTM by FUNCT_2:def 1;
   then pL.:cTM=rng pL by RELAT_1:113;
   then A47: rngPL is compact by B1,A23,A45,WEIERSTR:9;
   then A48: cRpL is compact by WEIERSTR:13;
   reconsider cRpL as non empty real-bounded Subset of REAL
   by A47,WEIERSTR:11,def 1;
   set L=lower_bound cRpL;
   L in cRpL by A48,RCOMP_1:14;
   then consider x be set such that
    A49: x in dom pL and
    A50: pL.x=L by A24,FUNCT_1:def 3;
   union G=[#]TM by A2,SETFAM_1:45;
   then consider Y be set such that
    A51: x in Y and
    A52: Y in rng g by A6,A49,TARSKI:def 4;
   reconsider x as Point of TM by A49;
   consider j be set such that
    A53: j in dom g and
    A54: g.j=Y by A52,FUNCT_1:def 3;
   reconsider j as Nat by A53;
   A55: j<=len g by A53,FINSEQ_3:25;
   A56: 1<=j by A53,FINSEQ_3:25;
   now per cases by A56,XXREAL_0:1;
    suppose A57: j=1;
     then not x in g19 by A51,A54,XBOOLE_0:def 5;
     then (dist_min g19).x<>0 by HAUSDORF:9;
     then (dist_min g19).x>0 by JORDAN1K:9;
     hence 0<L by A20,A21,A23,A25,A45,A50,A53,A55,A57;
    end;
    suppose A58: j>1;
     then reconsider j1=j-1 as Element of NAT by NAT_1:20;
     (p/.j1 is Element of FUNCS) & p/.j is Element of FUNCS;
     then reconsider pj1=p/.j1,pj=p/.j as Function of TM,R^1 by TOPMETR:17;
     j1+1>1 by A58;
     then A59: 1<=j1 & j1<len g by A55,NAT_1:13;
     then j1 in dom p by A20,FINSEQ_3:25;
     then A60: pj1 is continuous by A45;
     P[j1,pj1,pj] by A22,A25,A45,A53,A59;
     then consider A be non empty Subset of TM such that
      A61: A`=g.j and
      A62: for x be Point of TM holds pj.x=max(pj1.x,(dist_min A).x) by A60;
     A` is open by B2,A1,A6,A52,A54,A61,TOPS_2:def 1;
     then A63: A is closed by TOPS_1:3;
     not x in A by A51,A54,A61,XBOOLE_0:def 5;
     then (dist_min A).x<>0 by A63,HAUSDORF:9;
     then A64: (dist_min A).x>0 by JORDAN1K:9;
     pj.x=max(pj1.x,(dist_min A).x) by A62;
     then pj.x>0 by A64,XXREAL_0:25;
     hence 0<L by A20,A23,A25,A45,A50,A53,A55;
    end;
   end;
   then reconsider L as positive Real;
   take L;
   let X be Point of M;
   defpred P[Nat] means
    $1 in dom p & for f1 be Function of TM,R^1 st p/.$1=f1 holds f1.X>=L;
   pL.X in cRpL by A24,A46,FUNCT_1:def 3;
   then P[len p] by A8,A20,FINSEQ_3:25,XXREAL_2:3;
   then A65: ex k be Nat st P[k];
   consider k being Nat such that
    A66: P[k] and
    A67: for n be Nat st P[n] holds k<=n from NAT_1:sch 5(A65);
   A68: 1<=k by A66,FINSEQ_3:25;
   A69: k<=len p by A66,FINSEQ_3:25;
   per cases by A68,XXREAL_0:1;
   suppose A70: k=1;
    take g1;
    thus g1 in F by A1,A6,A10;
    let y be set such that
     A71: y in Ball(X,L);
    reconsider Y=y as Point of M by A71;
    A72: dist(X,Y)<L by A71,METRIC_1:11;
    assume not y in g1;
    then Y in g19 by XBOOLE_0:def 5;
    then A73: (dist_min g19).X<=dist(X,Y) by HAUSDORF:13;
    (dist_min g19).X>=L by A7,A21,A66,A70;
    hence contradiction by A72,A73,XXREAL_0:2;
   end;
   suppose A74: k>1;
    then reconsider k1=k-1 as Element of NAT by NAT_1:20;
    (p/.k1 is Element of FUNCS) & p/.k is Element of FUNCS;
    then reconsider pk1=p/.k1,pk=p/.k as Function of TM,R^1 by TOPMETR:17;
    k1+1>1 by A74;
    then A75: 1<=k1 & k1<len g by A20,A69,NAT_1:13;
    then k1 in dom p by A20,FINSEQ_3:25;
    then A76: pk1 is continuous by A45;
    P[k1,pk1,pk] by A22,A45,A66,A75;
    then consider A be non empty Subset of TM such that
     A77: A`=g.k and
     A78: for x be Point of TM holds pk.x=max(pk1.x,(dist_min A).x) by A76;
    take A`;
    A` in G by A6,A25,A66,A77,FUNCT_1:def 3;
    hence A` in F by A1;
    let y be set such that
     A79: y in Ball(X,L);
    reconsider Y=y as Point of M by A79;
    assume not y in A`;
    then Y in A by XBOOLE_0:def 5;
    then A80: (dist_min A).X<=dist(X,Y) by HAUSDORF:13;
    dist(X,Y)<L by A79,METRIC_1:11;
    then A81: (dist_min A).X<L by A80,XXREAL_0:2;
    A82: pk.X>=L by A66;
    pk.X=max(pk1.X,(dist_min A).X) by A78;
    then P[k1] by A20,A75,A81,A82,FINSEQ_3:25,XXREAL_0:16;
    then k1>=k1+1 by A67;
    hence contradiction by NAT_1:13;
   end;
  end;
 end;
end;

reserve L for Lebesgue_number of F;

theorem
  TopSpaceMetr M is compact & F is Cover of TopSpaceMetr M & F c= G
    implies L is Lebesgue_number of G
  proof
  assume that
   A1: TopSpaceMetr M is compact and
   A2: F is Cover of TopSpaceMetr M and
   A3: F c=G;
  A4: now let x be Point of M;
   ex A be Subset of TopSpaceMetr M st A in F & Ball(x,L)c=A by A1,A2,Def1;
   hence ex A be Subset of TopSpaceMetr M st A in G & Ball(x,L)c=A by A3;
  end;
  set TM=TopSpaceMetr M;
  union F=[#]TM & union F c=union G by A2,A3,SETFAM_1:45,ZFMISC_1:77;
  then G is Cover of TM by SETFAM_1:def 11;
  hence thesis by A1,A4,Def1;
 end;

theorem
  TopSpaceMetr M is compact & F is Cover of TopSpaceMetr M & F is_finer_than G
    implies L is Lebesgue_number of G
 proof
  assume that
   A1: TopSpaceMetr M is compact and
   A2: F is Cover of TopSpaceMetr M and
   A3: F is_finer_than G;
  set TM=TopSpaceMetr M;
  A4: now let x be Point of M;
   consider A be Subset of TopSpaceMetr M such that
    A5: A in F and
    A6: Ball(x,L)c=A by A1,A2,Def1;
   consider B be set such that
    A7: B in G and
    A8: A c=B by A3,A5,SETFAM_1:def 2;
   reconsider B as Subset of TM by A7;
   take B;
   thus B in G & Ball(x,L)c=B by A6,A7,A8,XBOOLE_1:1;
  end;
  union F=[#]TM & union F c=union G by A2,A3,SETFAM_1:13,45;
  then G is Cover of TM by SETFAM_1:def 11;
  hence thesis by A1,A4,Def1;
 end;

theorem
  for L1 be positive Real st TopSpaceMetr M is compact &
                             F is Cover of TopSpaceMetr M & L1 <= L
    holds L1 is Lebesgue_number of F
 proof
  let L9 be positive Real such that
   A1: (TopSpaceMetr M is compact) & F is Cover of TopSpaceMetr M and
   A2: L9<=L;
  now let x be Point of M;
   consider A be Subset of TopSpaceMetr M such that
    A3: A in F & Ball(x,L)c=A by A1,Def1;
   take A;
   Ball(x,L9)c=Ball(x,L) by A2,PCOMPS_1:1;
   hence A in F & Ball(x,L9)c=A by A3,XBOOLE_1:1;
  end;
  hence thesis by A1,Def1;
 end;

begin :: Bounded Simplicial Complexes

reserve n,k for Nat,
        r for real number,
        X for set,
        M for Reflexive non empty MetrStruct,
        A for Subset of M,
        K for SimplicialComplexStr;

registration let M;
  cluster finite -> bounded for Subset of M;
  coherence
  proof
  let A be Subset of M;
  per cases;
  suppose A is empty;
   hence thesis;
  end;
  suppose A1: A is non empty;
   assume A is finite;
   then reconsider a=A as finite non empty Subset of M by A1;
   deffunc D(Point of M,Point of M)=dist($1,$2);
   consider q be set such that
    A2: q in a by XBOOLE_0:def 1;
   set X={D(x,y) where x is Point of M,y is Point of M:x in a & y in a};
   reconsider q as Point of M by A2;
   A3: D(q,q) in X by A2;
   A4: now let x be set;
    assume x in X;
    then ex y be Point of M,z be Point of M st x=D(y,z) & y in a & z in a;
    hence x is real;
   end;
   A5: a is finite;
   X is finite from FRAENKEL:sch 22(A5,A5);
   then reconsider X as real-membered non empty finite set by A3,A4,
MEMBERED:def 3;
   reconsider sX=sup X as Real by XREAL_0:def 1;
   reconsider sX1=sX+1 as Real;
   take sX1;
   D(q,q)=0 & D(q,q)<=sX by A3,METRIC_1:1,XXREAL_2:4;
   hence 0<sX1;
   let x,y be Point of M;
   assume x in A & y in A;
   then D(x,y) in X;
   then D(x,y)<=sX by XXREAL_2:4;
   hence thesis by XREAL_1:39;
  end;
 end;
end;

theorem
  for S be finite non empty Subset of M
    ex p,q be Point of M st p in S & q in S & dist(p,q) = diameter S
 proof
  let S be finite non empty Subset of M;
  set q=the Element of S;
  reconsider q as Point of M;
  deffunc D(Point of M,Point of M)=dist($1,$2);
  set X={D(x,y) where x is Point of M,y is Point of M:x in S & y in S};
  A1: now let x be set;
   assume x in X;
   then ex y be Point of M,z be Point of M st x=D(y,z) & y in S & z in S;
   hence x is real;
  end;
  A2: D(q,q) in X;
  A3: S is finite;
  X is finite from FRAENKEL:sch 22(A3,A3);
  then reconsider X as real-membered non empty finite set by A1,A2,
MEMBERED:def 3;
  reconsider sX=sup X as Real by XREAL_0:def 1;
  sX in X by XXREAL_2:def 6;
  then consider p,q be Point of M such that
   A4: sX=D(p,q) & p in S & q in S;
  now let x,y be Point of M;
   assume x in S & y in S;
   then D(x,y) in X;
   hence D(x,y)<=sX by XXREAL_2:4;
  end;
  then A5: diameter S<=sX by TBSP_1:def 8;
  sX<=diameter S by A4,TBSP_1:def 8;
  hence thesis by A4,A5,XXREAL_0:1;
 end;

definition let M,K;
  attr K is M bounded means :Def2:
    ex r st for A st A in the topology of K holds
       A is bounded & diameter A <= r;
end;

theorem Th5:
  for K be non void SimplicialComplexStr st
      K is M bounded & A is Simplex of K
    holds A is bounded
 proof
  let K be non void SimplicialComplexStr;
  assume K is M bounded;
  then A1: ex r be real number st for A st A in the topology of K
    holds A is bounded & diameter A<=r by Def2;
  assume A is Simplex of K;
  then A in the topology of K by PRE_TOPC:def 2;
  hence thesis by A1;
 end;

registration let M,X;
  cluster M bounded non void for SimplicialComplex of X;
  existence
  proof
  set m=the Element of M;
  take K=Complex_of{{}X};
  K is M bounded
  proof
   take r=diameter{}M;
   let A;
   A1: the topology of K=bool{}X by SIMPLEX0:4;
   assume A in the topology of K;
   hence thesis by A1;
  end;
  hence thesis;
 end;
end;

registration let M;
  cluster M bounded non void subset-closed finite-membered
    for SimplicialComplexStr;
  existence
  proof
  take the M bounded non void SimplicialComplex of the set;
  thus thesis;
 end;
end;

registration let M,X;
  let K be M bounded SimplicialComplexStr of X;
  cluster -> M bounded for (SubSimplicialComplex of K);
  coherence
  proof
  let SK be SubSimplicialComplex of K;
  A1: the topology of SK c=the topology of K by SIMPLEX0:def 13;
  consider r be real number such that
   A2: for A st A in the topology of K holds A is bounded & diameter A<=r by
Def2;
  take r;
  let A;
  assume A in the topology of SK;
  hence thesis by A1,A2;
 end;
end;

registration
  let M,X;
  let K be M bounded subset-closed SimplicialComplexStr of X;
  let i be Integer;
  cluster Skeleton_of(K,i) -> M bounded;
  coherence;
end;

theorem Th6:
  K is finite-vertices implies K is M bounded
  proof
  set V=Vertices K;
  assume K is finite-vertices;
  then V is finite by SIMPLEX0:def 5;
  then reconsider VM=V/\[#]M as finite Subset of M;
  take diameter VM;
  let A;
  assume A1: A in the topology of K;
  then reconsider S=A as Subset of K;
  S is simplex-like by A1,PRE_TOPC:def 2;
  then A c=V by SIMPLEX0:17;
  then A c=VM by XBOOLE_1:19;
  hence thesis by TBSP_1:24;
 end;

begin :: The Diameter of a Bounded Simplicial Complex

Lm1: 0 in REAL by XREAL_0:def 1;

definition let M;
  let K be SimplicialComplexStr such that
    B1: K is M bounded;
  func diameter(M,K) -> Real means :Def3:
    (for A st A in the topology of K holds diameter A <= it)
  &  for r st (for A st A in the topology of K holds diameter A <= r)
     holds r >= it if the topology of K meets bool [#]M
                   otherwise it = 0;
 existence
 proof
  the topology of K meets bool[#]M implies ex d be Real st(for A st A in the
topology of K holds diameter A<=d) & for r be real number st(for A st A in the
topology of K holds diameter A<=r) holds r>=d
  proof
   defpred P[Subset of M] means
    $1 in the topology of K & $1 is bounded;
   deffunc D(Subset of M)=diameter$1;
   set X={D(S) where S is Subset of M:P[S]};
   now let x be set;
    assume x in X;
    then ex S be Subset of M st x=D(S) & P[S];
    hence x is real;
   end;
   then reconsider X as real-membered set by MEMBERED:def 3;
   assume the topology of K meets bool[#]M;
   then consider B be set such that
    A1: B in the topology of K and
    A2: B in bool[#]M by XBOOLE_0:3;
   reconsider B as Subset of M by A2;
   consider rr be real number such that
    A3: for A st A in the topology of K holds A is bounded & D(A)<=rr by B1
,Def2;
   now let x be ext-real number;
    assume x in X;
    then consider s be Subset of M such that
     A4: x=D(s) & P[s];
    thus x<=rr by A3,A4;
   end;
   then rr is UpperBound of X by XXREAL_2:def 1;
   then A5: X is bounded_above by XXREAL_2:def 10;
   B is bounded by A1,A3;
   then D(B) in X by A1;
   then reconsider sX=sup X as Real by A5,XXREAL_2:16;
   take sX;
   hereby let A;
    assume A in the topology of K;
    then P[A] by A3;
    then D(A) in X;
    hence D(A)<=sX by XXREAL_2:4;
   end;
   let r be real number such that
    A6: for A st A in the topology of K holds diameter A<=r;
   now let x be ext-real number;
    assume x in X;
    then consider A such that
     A7: x=D(A) & P[A];
    thus x<=r by A6,A7;
   end;
   then r is UpperBound of X by XXREAL_2:def 1;
   hence thesis by XXREAL_2:def 3;
  end;
  hence thesis by Lm1;
 end;
 uniqueness
 proof
  now let r1,r2 be Real such that
    A8: (for A st A in the topology of K holds diameter A<=r1) & ((for r be
real number st(for A st A in the topology of K holds diameter A<=r) holds r>=r1
) & for A st A in the topology of K holds diameter A<=r2) & for r be real
number st(for A st A in the topology of K holds diameter A<=r) holds r>=r2;
   r1<=r2 & r2<=r1 by A8;
   hence r1=r2 by XXREAL_0:1;
  end;
  hence thesis;
 end;
 consistency;
end;

theorem Th7:
  K is M bounded implies 0 <= diameter(M,K)
 proof
  assume A1: K is M bounded;
  per cases;
  suppose A2: the topology of K meets bool[#]M;
   then consider S be set such that
    A3: S in the topology of K and
    A4: S in bool[#]M by XBOOLE_0:3;
   reconsider S as Subset of M by A4;
   ex r be real number st for A st A in the topology of K holds A is bounded &
diameter A<=r by A1,Def2;
   then diameter S>=0 by A3,TBSP_1:21;
   hence thesis by A1,A2,A3,Def3;
  end;
  suppose the topology of K misses bool[#]M;
   hence thesis by A1,Def3;
  end;
 end;

theorem
  for K be M bounded SimplicialComplexStr of X,
      KX be SubSimplicialComplex of K
    holds diameter(M,KX) <= diameter(M,K)
 proof
  let K be M bounded SimplicialComplexStr of X,KX be SubSimplicialComplex of K;
  A1: the topology of KX c=the topology of K by SIMPLEX0:def 13;
  per cases;
  suppose A2: the topology of KX meets bool[#]M;
   then the topology of K meets bool[#]M by A1,XBOOLE_1:63;
   then for A st A in the topology of KX holds diameter A<=diameter(M,K) by A1
,Def3;
   hence thesis by A2,Def3;
  end;
  suppose the topology of KX misses bool[#]M;
   then diameter(M,KX)=0 by Def3;
   hence thesis by Th7;
  end;
 end;

theorem
  for K be M bounded subset-closed SimplicialComplexStr of X,i be Integer
    holds
  diameter(M,Skeleton_of(K,i)) <= diameter(M,K)
 proof
  set r = the Real;
  let K be M bounded subset-closed SimplicialComplexStr of X,i be Integer;
  set SK=Skeleton_of(K,i);
  A1: the topology of SK c=the topology of K by SIMPLEX0:def 13;
  per cases;
  suppose A2: the topology of SK meets bool[#]M;
   then A3: the topology of K meets bool[#]M by A1,XBOOLE_1:63;
   now let A;
    the_family_of K is subset-closed by MATROID0:def 3;
    then A4: the topology of K is subset-closed by MATROID0:def 1;
    assume A in the topology of SK;
    then consider w be set such that
     A5: A c=w and
     A6: w in the_subsets_with_limited_card(i+1,the topology of K) by
SIMPLEX0:2;
    reconsider w as Subset of K by A6;
    w in the topology of K by A6,SIMPLEX0:def 2;
    then A in the topology of K by A4,A5,CLASSES1:def 1;
    hence diameter A<=diameter(M,K) by A3,Def3;
   end;
   hence thesis by A2,Def3;
  end;
  suppose the topology of SK misses bool[#]M;
   then diameter(M,SK)=0 by Def3;
   hence thesis by Th7;
  end;
 end;

definition let M;
 let K be M bounded non void subset-closed SimplicialComplexStr;
 redefine func diameter(M,K) -> Real means :Def4:
  (for A st A is Simplex of K holds diameter A <= it) &
  for r st (for A st A is Simplex of K holds diameter A <= r)
    holds r >= it;
 coherence;
 compatibility
 proof
  let d be Real;
  {}K is simplex-like;
  then {}M in the topology of K by PRE_TOPC:def 2;
  then A1: the topology of K meets bool[#]M by XBOOLE_0:3;
  hereby assume A2: d=diameter(M,K);
   hereby let A;
    assume A is Simplex of K;
    then A in the topology of K by PRE_TOPC:def 2;
    hence diameter A<=d by A1,A2,Def3;
   end;
   let r be real number;
   assume A3: for A st A is Simplex of K holds diameter A<=r;
   now let A;
    assume A in the topology of K;
    then A is Simplex of K by PRE_TOPC:def 2;
    hence diameter A<=r by A3;
   end;
   hence r>=d by A1,A2,Def3;
  end;
  assume that
   A4: for A st A is Simplex of K holds diameter A<=d and
   A5: for r be real number st(for A st A is Simplex of K holds diameter A<=r)
holds r>=d;
  now let A;
   assume A in the topology of K;
   then A is Simplex of K by PRE_TOPC:def 2;
   hence diameter A<=d by A4;
  end;
  then A6: diameter(M,K)<=d by A1,Def3;
  now let A;
   assume A is Simplex of K;
   then A in the topology of K by PRE_TOPC:def 2;
   hence diameter A<=diameter(M,K) by A1,Def3;
  end;
  then d<=diameter(M,K) by A5;
  hence d=diameter(M,K) by A6,XXREAL_0:1;
 end;
end;

theorem
  for S be finite Subset of M holds diameter(M,Complex_of{S}) = diameter S
 proof
  let S be finite Subset of M;
  set C=Complex_of{S};
  reconsider C as M bounded non void SimplicialComplex of M by Th6;
  reconsider s=S as Subset of C;
  A1: the topology of C=bool S by SIMPLEX0:4;
  now let W be Subset of M;
   assume W is Simplex of C;
   then W in bool S by A1,PRE_TOPC:def 2;
   hence diameter W<=diameter S by TBSP_1:24;
  end;
  then A2: diameter(M,C)<=diameter S by Def4;
  S c=S;
  then s is simplex-like by A1,PRE_TOPC:def 2;
  then diameter S<=diameter(M,C) by Def4;
  hence thesis by A2,XXREAL_0:1;
 end;

definition
 let n;
 let K be SimplicialComplexStr of TOP-REAL n;
 attr K is bounded means :Def5:
   K is (Euclid n) bounded;
 func diameter K -> Real equals
   diameter(Euclid n,K);
 coherence;
end;

registration
  let n;
  cluster bounded -> Euclid n bounded for (SimplicialComplexStr of TOP-REAL n);
  coherence by Def5;
  cluster bounded affinely-independent simplex-join-closed non void
    finite-degree total for SimplicialComplex of TOP-REAL n;
  existence
  proof
  set T=TOP-REAL n;
  take C=Complex_of{{}TOP-REAL n};
  C is Euclid n bounded by Th6;
  hence thesis by Def5;
 end;
  cluster finite-vertices -> bounded for SimplicialComplexStr of TOP-REAL n;
  coherence
  proof
  let K be SimplicialComplexStr of TOP-REAL n;
  assume K is finite-vertices;
  then K is Euclid n bounded by Th6;
  hence thesis by Def5;
 end;
end;

Lm2: [#]TOP-REAL n=[#]Euclid n
 proof
  the TopStruct of TOP-REAL n=TopSpaceMetr Euclid n by EUCLID:def 8;
  hence thesis;
 end;

begin :: The Estimation of Diameter of the Barycentric Subdivision

reserve V for RealLinearSpace,
        Kv for non void SimplicialComplex of V;

Lm3: for x be set holds {x} is c=-linear
 proof
  let x be set;
  let y,z be set;
  assume that
   A1: y in {x} and
   A2: z in {x};
  y=x by A1,TARSKI:def 1;
  hence thesis by A2,TARSKI:def 1;
 end;

theorem Th11:
  for S be Simplex of BCS Kv
  for F be c=-linear finite finite-membered Subset-Family of V st
    S = (center_of_mass V).:F
  for a1,a2 be VECTOR of V st a1 in S & a2 in S
  ex b1,b2 be VECTOR of V,r be Real st
     b1 in Vertices BCS Complex_of{union F} &
     b2 in Vertices BCS Complex_of{union F} &
     a1-a2 = r*(b1-b2) & 0 <= r & r <= (card union F-1)/card union F
 proof
  let S be Simplex of BCS Kv;
  set cM=center_of_mass V;
  let F be c=-linear finite finite-membered Subset-Family of V such that
   A1: S=cM.:F;
  let a1,a2 be VECTOR of V such that
   A2: a1 in S and
   A3: a2 in S;
  consider A1 be set such that
   A4: A1 in dom cM and
   A5: A1 in F and
   A6: cM.A1=a1 by A1,A2,FUNCT_1:def 6;
  consider A2 be set such that
   A7: A2 in dom cM and
   A8: A2 in F and
   A9: cM.A2=a2 by A1,A3,FUNCT_1:def 6;
  A10: A1,A2 are_c=-comparable by A5,A8,ORDINAL1:def 8;
  set uF=union F;
  set CuF=Complex_of{uF};
  A11: for a1,a2 be VECTOR of V for A1,A2 be set st A1 c=A2 & A1 in dom cM & A1
in F & cM.A1=a1 & A1 in dom cM & A2 in F & cM.A2=a2 ex b1,b2 be VECTOR of V,r
be Real st b1 in Vertices BCS CuF & b2 in Vertices BCS CuF & a1-a2=r*(b1-b2) &
0<=r & r<=(card uF-1)/card uF
  proof
   let a1,a2 be VECTOR of V;
   A12: the topology of CuF=bool uF by SIMPLEX0:4;
   let A1,A2 be set such that
    A13: A1 c=A2 and
    A14: A1 in dom cM and
    A15: A1 in F and
    A16: cM.A1=a1 and
    A1 in dom cM and
    A17: A2 in F and
    A18: cM.A2=a2;
   A19: A1 c=uF by A15,ZFMISC_1:74;
   A20: A1<>{} by A14,ORDERS_1:1;
   then A21: uF is non empty by A19;
   A22: A2 c=uF by A17,ZFMISC_1:74;
   reconsider A1,A2 as non empty finite Subset of V by A13,A15,A17,A20;
   set A21=A2\A1;
   reconsider AA1={A1},AA2={A21} as Subset-Family of CuF;
   {A1}c=bool uF by A19,ZFMISC_1:31;
   then A23: AA1 is c=-linear finite simplex-like by A12,Lm3,SIMPLEX0:14;
   A21 c=A2 by XBOOLE_1:36;
   then A21 c=uF by A22,XBOOLE_1:1;
   then {A21}c=bool uF by ZFMISC_1:31;
   then A24: AA2 is c=-linear finite simplex-like by A12,Lm3,SIMPLEX0:14;
   A25: |.CuF.|c=[#]V;
   [#]CuF=[#]V;
   then A26: BCS CuF=subdivision(cM,CuF) by A25,SIMPLEX1:def 5;
   A27: [#]subdivision(cM,CuF)=[#]CuF by SIMPLEX0:def 20;
   then reconsider aa1={a1} as Subset of BCS CuF by A25,SIMPLEX1:def 5;
   A28: a1 in aa1 by TARSKI:def 1;
   then reconsider d1=a1 as Element of BCS CuF;
   A29: dom cM=BOOL the carrier of V by FUNCT_2:def 1;
   cM.:AA1=Im(cM,A1) by RELAT_1:def 16
    .={a1} by A14,A16,FUNCT_1:59;
   then aa1 is simplex-like by A23,A26,SIMPLEX0:def 20;
   then A30: d1 is vertex-like by A28,SIMPLEX0:def 3;
   per cases;
   suppose A31: A1=A2;
    reconsider Z=0 as Real by XREAL_0:def 1;
    take b1=a1,b2=a1,Z;
    card uF>=1 by A21,NAT_1:14;
    then A32: card uF-1>=1-1 by XREAL_1:6;
    a1-a2=0.V by A16,A18,A31,RLVECT_1:5;
    hence thesis by A30,A32,RLVECT_1:10,SIMPLEX0:def 4;
   end;
   suppose A1<>A2;
    then not A2 c=A1 by A13,XBOOLE_0:def 10;
    then reconsider A21 as non empty finite Subset of V by XBOOLE_1:37;
    A33: A21 in dom cM by A29,ORDERS_1:2;
    then cM.A21 in rng cM by FUNCT_1:def 3;
    then reconsider a21=cM.A21 as VECTOR of V;
    reconsider aa2={a21} as Subset of BCS CuF by A25,A27,SIMPLEX1:def 5;
    A34: a21 in aa2 by TARSKI:def 1;
    then reconsider d2=a21 as Element of BCS CuF;
    cM.:AA2=Im(cM,A21) by RELAT_1:def 16
     .={a21} by A33,FUNCT_1:59;
    then aa2 is simplex-like by A24,A26,SIMPLEX0:def 20;
    then A35: d2 is vertex-like by A34,SIMPLEX0:def 3;
    set r1=1/card A1,r2=1/card A2,r21=1/card A21,r=card A21/card A2;
    reconsider r1,r2,r21,r as Real by XREAL_0:def 1;
    take a1,a21,r;
    A36: r*r21=(card A21*1)/(card A21*card A2) by XCMPLX_1:76
     .=r2 by XCMPLX_1:91;
    consider L1 be Linear_Combination of A1 such that
     A37: Sum L1=r1*Sum A1 and
     sum L1=r1*card A1 and
     A38: L1=(ZeroLC V)+*(A1-->r1) by RLAFFIN2:15;
    A39: Carrier(L1)c=A1 by RLVECT_2:def 6;
    A40: card A21=1 *card A2-1 *card A1 by A13,CARD_2:44;
    then A41: r1-r2=(card A21*1)/(card A2*card A1) by XCMPLX_1:130
     .=r*r1 by XCMPLX_1:76;
    consider L21 be Linear_Combination of A21 such that
     A42: Sum L21=r21*Sum A21 and
     sum L21=r21*card A21 and
     A43: L21=(ZeroLC V)+*(A21-->r21) by RLAFFIN2:15;
    A44: Carrier(L21)c=A21 by RLVECT_2:def 6;
    consider L2 be Linear_Combination of A2 such that
     A45: Sum L2=r2*Sum A2 and
     sum L2=r2*card A2 and
     A46: L2=(ZeroLC V)+*(A2-->r2) by RLAFFIN2:15;
    A47: Carrier(L2)c=A2 by RLVECT_2:def 6;
    for v be Element of V holds(L1-L2).v=(r*(L1-L21)).v
    proof
     let v be Element of V;
     A48: dom(A21-->r21)=A21 by FUNCOP_1:13;
     A49: (L1-L2).v=L1.v-L2.v by RLVECT_2:54;
     A50: dom(A1-->r1)=A1 by FUNCOP_1:13;
     A51: dom(A2-->r2)=A2 by FUNCOP_1:13;
     (r*(L1-L21)).v=r*((L1-L21).v) by RLVECT_2:def 11;
     then A52: (r*(L1-L21)).v=r*(L1.v-L21.v) by RLVECT_2:54;
     per cases;
     suppose A53: v in A1;
      then not v in Carrier(L21) by A44,XBOOLE_0:def 5;
      then A54: L21.v=0 by RLVECT_2:19;
      A55: (A2-->r2).v=r2 & (A1-->r1).v=r1 by A13,A53,FUNCOP_1:7;
      L1.v=(A1-->r1).v by A38,A50,A53,FUNCT_4:13;
      hence thesis by A13,A41,A46,A49,A51,A52,A53,A54,A55,FUNCT_4:13;
     end;
     suppose A56: v in A2 & not v in A1;
      then not v in Carrier L1 by A39;
      then A57: L1.v=0 by RLVECT_2:19;
      (A2-->r2).v=r2 by A56,FUNCOP_1:7;
      then A58: (L1-L2).v=-r2 by A46,A49,A51,A56,A57,FUNCT_4:13;
      A59: v in A21 by A56,XBOOLE_0:def 5;
      then (A21-->r21).v=r21 by FUNCOP_1:7;
      then (r*(L1-L21)).v=r*(-r21) by A43,A48,A52,A57,A59,FUNCT_4:13;
      hence thesis by A36,A58;
     end;
     suppose A60: not v in A1 & not v in A2;
      then not v in Carrier(L1) by A39;
      then A61: L1.v=0 by RLVECT_2:19;
      not v in Carrier(L21) by A44,A60,XBOOLE_0:def 5;
      then A62: L21.v=0 by RLVECT_2:19;
      not v in Carrier(L2) by A47,A60;
      hence thesis by A49,A52,A62,A61,RLVECT_2:19;
     end;
    end;
    then A63: L1-L2=r*(L1-L21) by RLVECT_2:def 9;
    card A1>=1 & card A2<=card uF by A17,NAT_1:14,43,ZFMISC_1:74;
    then card A1*card uF>=1 *card A2 by XREAL_1:66;
    then card A2*card uF-card A1*card uF<=card uF*card A2-card A2 by XREAL_1:13
;
    then A64: card A21*card uF<=(card uF-1)*card A2 by A40;
    A65: Sum L21=a21 by A42,RLAFFIN2:def 2;
    A66: Sum L1=a1 by A16,A37,RLAFFIN2:def 2;
    Sum L2=a2 by A18,A45,RLAFFIN2:def 2;
    then a1-a2=Sum(r*(L1-L21)) by A63,A66,RLVECT_3:4
     .=r*Sum(L1-L21) by RLVECT_3:2
     .=r*(a1-a21) by A65,A66,RLVECT_3:4;
    hence thesis by A21,A30,A35,A64,SIMPLEX0:def 4,XREAL_1:102;
   end;
  end;
  per cases by A10,XBOOLE_0:def 9;
  suppose A1 c=A2;
   hence thesis by A4,A5,A6,A8,A9,A11;
  end;
  suppose A2 c=A1;
   then consider b1,b2 be VECTOR of V,r be Real such that
    A67: b1 in Vertices BCS CuF & b2 in Vertices BCS CuF and
    A68: a2-a1=r*(b1-b2) and
    A69: 0<=r & r<=(card uF-1)/card uF by A5,A6,A7,A8,A9,A11;
   take b2,b1,r;
   a1-a2=-(r*(b1-b2)) by A68,RLVECT_1:33
    .=r*(-(b1-b2)) by RLVECT_1:25
    .=r*(b2-b1) by RLVECT_1:33;
   hence thesis by A67,A69;
  end;
 end;

theorem Th12:
  for A be affinely-independent Subset of TOP-REAL n
  for E be Enumeration of A st dom E\X is non empty
    holds
  conv(E.:X) = meet{conv(A\{E.k}) where k is Element of NAT: k in dom E\X}
  proof
  let A be affinely-independent Subset of TOP-REAL n;
  let E be Enumeration of A such that
   A1: dom E\X is non empty;
  set d=dom E;
  defpred P[Nat] means
   $1<>0 implies for X st card((dom E)\X)=$1 holds conv(A\E.:(d\X))=meet{conv(A
\{E.k}) where k is Element of NAT:k in dom E\X};
  A2: rng E=A by RLAFFIN3:def 1;
  A3: for i be Nat st P[i] holds P[i+1]
  proof
   deffunc C(set)=conv(A\{E.$1});
   let i be Nat;
   assume A4: P[i];
   set i1=i+1;
   assume i1<>0;
   let X;
   set U={C(k) where k is Element of NAT:k in d\X};
   assume A5: card(d\X)=i1;
   then d\X is non empty;
   then consider m be set such that
    A6: m in d\X by XBOOLE_0:def 1;
   A7: m in d by A6,XBOOLE_0:def 5;
   reconsider m as Element of NAT by A6;
   A8: E.:{m}=Im(E,m) by RELAT_1:def 16
    .={E.m} by A7,FUNCT_1:59;
   per cases;
   suppose i=0;
    then consider x be set such that
     A9: d\X={x} by A5,CARD_2:42;
    A10: x=m by A6,A9,TARSKI:def 1;
    A11: U c={C(m)}
    proof
     let u be set;
     assume u in U;
     then ex k be Element of NAT st u=C(k) & k in d\X;
     then u=C(m) by A9,A10,TARSKI:def 1;
     hence thesis by TARSKI:def 1;
    end;
    C(m) in U by A6;
    then A12: U={C(m)} by A11,ZFMISC_1:33;
    E.:(d\X)={E.m} by A6,A8,A9,TARSKI:def 1;
    hence thesis by A12,SETFAM_1:10;
   end;
   suppose A13: i>0;
    set Xm=X\/{m};
    set Um={C(k) where k is Element of NAT:k in d\Xm};
    set t=the Element of(d\Xm);
    A14: d\X\{m}\/{m}=d\X by A6,ZFMISC_1:116;
    A15: d\X\{m}=d\Xm by XBOOLE_1:41;
    A16: Um c=U
    proof
     let x be set;
     assume x in Um;
     then consider k be Element of NAT such that
      A17: x=C(k) and
      A18: k in d\Xm;
     k in d\X by A15,A14,A18,XBOOLE_0:def 3;
     hence thesis by A17;
    end;
    m in {m} by TARSKI:def 1;
    then not m in d\X\{m} by XBOOLE_0:def 5;
    then A19: card(d\X\{m})+1=card(d\X) by A14,CARD_2:41;
    then d\Xm is non empty by A5,A13,A15;
    then t in d\Xm;
    then A20: C(t) in Um;
    set c =C(m),CC={c};
    set CA=Complex_of{A};
    A21: the topology of CA =bool A by SIMPLEX0:4;
    A22: U c=Um\/CC
    proof
     let x be set;
     assume x in U;
     then consider k be Element of NAT such that
      A23: x=C(k) and
      A24: k in d\X;
     k in d\Xm or k in {m} by A15,A14,A24,XBOOLE_0:def 3;
     then k in d\Xm or k=m by TARSKI:def 1;
     then x in Um or x in CC by A23,TARSKI:def 1;
     hence thesis by XBOOLE_0:def 3;
    end;
    C(m) in U by A6;
    then CC c=U by ZFMISC_1:31;
    then A25: Um\/CC c=U by A16,XBOOLE_1:8;
    reconsider A1=A\E.:(d\Xm),A2=A\{E.m} as Subset of CA;
    A\{E.m}c=A by XBOOLE_1:36;
    then A26: A2 is simplex-like by A21,PRE_TOPC:def 2;
    A\E.:(d\Xm)c=A by XBOOLE_1:36;
    then A1 is simplex-like by A21,PRE_TOPC:def 2;
    then A27: conv@A1/\conv@A2=conv@(A1/\A2) by A26,SIMPLEX1:def 8;
    E.:(d\Xm)\/{E.m} =E.:((d\Xm)\/{m}) by A8,RELAT_1:120
     .=E.:(d\X) by A14,XBOOLE_1:41;
    then A28: A1/\A2=A\E.:(d\X) by XBOOLE_1:53;
    conv(A\E.:(d\Xm))=meet Um by A4,A5,A13,A15,A19;
    then conv(A\E.:(d\X))=meet Um/\meet CC by A28,A27,SETFAM_1:10
     .=meet(Um\/CC) by A20,SETFAM_1:9;
    hence thesis by A25,A22,XBOOLE_0:def 10;
   end;
  end;
  A29: P[0];
  for i be Nat holds P[i] from NAT_1:sch 2(A29,A3);
  then A30: P[card(d\X)];
  d\(d\X)=d/\X by XBOOLE_1:48;
  then E.:X=E.:(d\(d\X)) by RELAT_1:112
   .=E.:d\E.:(d\X) by FUNCT_1:64
   .=A\E.:(d\X) by A2,RELAT_1:113;
  hence thesis by A1,A30;
 end;

reserve A for Subset of TOP-REAL n;

theorem Th13:
  for a be bounded Subset of Euclid n st a=A
  for p be Point of Euclid n st p in conv A holds
    conv A c= cl_Ball(p,diameter a)
  proof
  A1: n in NAT by ORDINAL1:def 12;
  A2: the TopStruct of TOP-REAL n=TopSpaceMetr Euclid n by EUCLID:def 8;
  let a be bounded Subset of Euclid n
     such that
   A3: A=a;
  let x be Point of Euclid n such that
   A4: x in conv A;
  A5: A c=cl_Ball(x,diameter a)
  proof
   let p be set;
   assume A6: p in A;
   then reconsider p as Point of Euclid n by A3;
   reconsider pp=p as Point of TOP-REAL n by A2;
   A7: cl_Ball(p,diameter a)=cl_Ball(pp,diameter a) by A1,TOPREAL9:14;
   A c=cl_Ball(p,diameter a)
   proof
    let y be set;
    assume A8: y in A;
    then reconsider q=y as Point of Euclid n by A3;
    dist(p,q)<=diameter a by A3,A6,A8,TBSP_1:def 8;
    hence thesis by METRIC_1:12;
   end;
   then conv A c=cl_Ball(pp,diameter a) by A7,CONVEX1:30;
   then dist(p,x)<=diameter a by A4,A7,METRIC_1:12;
   hence thesis by METRIC_1:12;
  end;
  reconsider xx=x as Point of TOP-REAL n by A2;
  cl_Ball(x,diameter a)=cl_Ball(xx,diameter a) by A1,TOPREAL9:14;
  hence thesis by A5,CONVEX1:30;
 end;

theorem Th14:
  A is bounded iff conv A is bounded
  proof
  the TopStruct of TOP-REAL n=TopSpaceMetr Euclid n by EUCLID:def 8;
  then reconsider cA=conv A,a=A as Subset of Euclid n;
  hereby assume A is bounded;
   then reconsider a as bounded Subset of Euclid n by JORDAN2C:11;
   set D=diameter a;
   A1: now let x,y be Point of Euclid n;
    assume x in cA;
    then A2: conv A c=cl_Ball(x,D) by Th13;
    assume y in cA;
    then dist(x,y)<=D by A2,METRIC_1:12;
    hence dist(x,y)<=D+1 by XREAL_1:39;
   end;
   D>=0 by TBSP_1:21;
   then cA is bounded by A1,TBSP_1:def 7;
   hence conv A is bounded by JORDAN2C:11;
  end;
  assume conv A is bounded;
  then cA is bounded by JORDAN2C:11;
  then a is bounded by CONVEX1:41,TBSP_1:14;
  hence thesis by JORDAN2C:11;
 end;

theorem Th15:
  for a,ca be bounded Subset of Euclid n st ca = conv A & a = A holds
    diameter a = diameter ca
 proof
  let a,ca be bounded Subset of Euclid n;
  assume that
   A1: ca=conv A and
   A2: a=A;
  per cases;
  suppose a is empty;
   hence thesis by A1,A2;
  end;
  suppose A3: a is non empty;
   now let x,y be Point of Euclid n;
    assume x in ca;
    then A4: conv A c=cl_Ball(x,diameter a) by A1,A2,Th13;
    assume y in ca;
    hence dist(x,y)<=diameter a by A1,A4,METRIC_1:12;
   end;
   then A5: diameter ca<=diameter a by A1,A2,A3,TBSP_1:def 8;
   diameter a<=diameter ca by A1,A2,CONVEX1:41,TBSP_1:24;
   hence thesis by A5,XXREAL_0:1;
  end;
 end;

registration
  let n;
  let K be bounded SimplicialComplexStr of TOP-REAL n;
  cluster -> bounded for SubdivisionStr of K;
  coherence
  proof
  let SK be SubdivisionStr of K;
  consider r be real number such that
   A1: for A be Subset of Euclid n st A in the topology of K holds A is bounded
& diameter A<=r by Def2;
  take r;
  let A be Subset of Euclid n;
  assume A2: A in the topology of SK;
  then reconsider a=A as Subset of SK;
  a is simplex-like by A2,PRE_TOPC:def 2;
  then consider b be Subset of K such that
   A3: b is simplex-like and
   A4: conv@a c=conv@b by SIMPLEX1:def 4;
  A5: [#]TOP-REAL n=[#]Euclid n by Lm2;
  then reconsider cA=conv@a as Subset of Euclid n;
  [#]K c=[#]TOP-REAL n by SIMPLEX0:def 9;
  then reconsider B=b as Subset of Euclid n by A5,XBOOLE_1:1;
  A6: B in the topology of K by A3,PRE_TOPC:def 2;
  then A7: diameter B<=r by A1;
  A8: B is bounded by A1,A6;
  then @b is bounded by JORDAN2C:11;
  then conv@b is bounded by Th14;
  then reconsider cB=conv@b as bounded Subset of Euclid n by JORDAN2C:11;
  A9: diameter cA<=diameter cB by A4,TBSP_1:24;
  cA c=cB by A4;
  then A10: cA is bounded by TBSP_1:14;
  then A is bounded by CONVEX1:41,TBSP_1:14;
  then A11: diameter cA=diameter A by A10,Th15;
  diameter cB=diameter B by A8,Th15;
  hence thesis by A9,A10,A11,A7,CONVEX1:41,TBSP_1:14,XXREAL_0:2;
 end;
end;

theorem Th16:
  for K be bounded finite-degree non void SimplicialComplex of TOP-REAL n st
       |.K.| c= [#]K
    holds diameter BCS K <= degree K/(degree K+1) * diameter K
  proof
  set T=TOP-REAL n;
  let K be bounded finite-degree non void SimplicialComplex of T;
  set BK=BCS K;
  set cM=center_of_mass T;
  set dK=degree K;
  assume |.K.|c=[#]K;
  then A1: BCS K=subdivision(cM,K) by SIMPLEX1:def 5;
  for A be Subset of Euclid n st A is Simplex of BK holds diameter A<=dK/(dK+1)
*diameter K
  proof
   let A be Subset of Euclid n;
   reconsider ONE=1 as ext-real number;
   assume A2: A is Simplex of BK;
   then reconsider a=A as Simplex of BK;
   consider S be c=-linear finite simplex-like Subset-Family of K such that
    A3: A=cM.:S by A1,A2,SIMPLEX0:def 20;
   A4: A is bounded by A2,Th5;
   reconsider s=@S as c=-linear finite finite-membered Subset-Family of T;
   set Us=union s;
   set C=Complex_of{Us};
   union S is empty or union S in S by SIMPLEX0:9,ZFMISC_1:2;
   then A5: union S is simplex-like by TOPS_2:def 1;
   then A6: card union S<=degree K+ONE by SIMPLEX0:24;
   A7: diameter K>=0 by Th7;
   A8: not{} in dom cM by ORDERS_1:1;
   then A9: dom cM is with_non-empty_elements by SETFAM_1:def 8;
   A10: [#]T=[#]Euclid n by Lm2;
   then reconsider US=Us as Subset of Euclid n;
   A11: a in the topology of BK by PRE_TOPC:def 2;
   per cases;
   suppose K is empty-membered;
    then A12: dK=-1 by SIMPLEX0:22;
    then -1<=degree BK & degree BK<=-1 by A1,A9,SIMPLEX0:23,52;
    then degree BK=-1 by XXREAL_0:1;
    then BK is empty-membered by SIMPLEX0:22;
    then the topology of BK is empty-membered by SIMPLEX0:def 7;
    then A13: a={} by A11,SETFAM_1:def 10;
    dK/(dK+1)=0 by A12;
    hence thesis by A13,TBSP_1:def 8;
   end;
   suppose K is non empty-membered;
    then degree K>=-1 & dK<>-1 by SIMPLEX0:22,23;
    then dK>-1 by XXREAL_0:1;
    then A14: dK>=-1+1 by INT_1:7;
    then A15: dK/(dK+1)*diameter K>=0 by A7;
    per cases;
    suppose a is empty;
     hence thesis by A15,TBSP_1:def 8;
    end;
    suppose A16: a is non empty;
     now US is bounded;
      then Us is bounded by JORDAN2C:11;
      then conv Us is bounded by Th14;
      then reconsider cUs=conv Us as bounded Subset of Euclid n by JORDAN2C:11;
      let x,y be Point of Euclid n;
      assume that
       A17: x in A and
       A18: y in A;
      reconsider X=x,Y=y as Element of T by A10;
      A19: |.BCS C.|=|.C.| & |.C.|=conv Us by SIMPLEX1:8,10;
      consider p be set such that
       A20: p in dom cM and
       A21: p in s and
       cM.p=x by A3,A17,FUNCT_1:def 6;
      p c=Us by A21,ZFMISC_1:74;
      then A22: Us<>{} by A8,A20;
      card Us<=dK+1 by A6,XXREAL_3:def 2;
      then A23: (dK+1)"<=(card Us)" by A22,XREAL_1:85;
      A24: diameter US<=diameter K by A5,Def4;
      A25: (card Us-1)/card Us=card Us/card Us-(1/card Us)
       .=1-(1/card Us) by A22,XCMPLX_1:60;
      A26: diameter cUs=diameter US by Th15;
      consider b1,b2 be VECTOR of T,r be Real such that
       A27: b1 in Vertices BCS C and
       A28: b2 in Vertices BCS C and
       A29: X-Y=r*(b1-b2) and
       A30: 0<=r and
       A31: r<=(card Us-1)/card Us by A3,A16,A17,A18,Th11;
      reconsider B1=b1,B2=b2 as Element of BCS C by A27,A28;
      B1 is vertex-like by A27,SIMPLEX0:def 4;
      then consider S1 be Subset of BCS C such that
       A32: S1 is simplex-like and
       A33: B1 in S1 by SIMPLEX0:def 3;
      A34: conv@S1 c=|.BCS C.| by A32,SIMPLEX1:5;
      B2 is vertex-like by A28,SIMPLEX0:def 4;
      then consider S2 be Subset of BCS C such that
       A35: S2 is simplex-like and
       A36: B2 in S2 by SIMPLEX0:def 3;
      @S2 c=conv@S2 by CONVEX1:41;
      then A37: B2 in conv@S2 by A36;
      @S1 c=conv@S1 by CONVEX1:41;
      then A38: B1 in conv@S1 by A33;
      reconsider bb1=b1,bb2=b2 as Point of Euclid n by A10;
      dK/(dK+1)=(dK+1)/(dK+1)-(1/(dK+1))
       .=1-(1/(dK+1)) by A14,XCMPLX_1:60;
      then (card Us-1)/card Us<=dK/(dK+1) by A23,A25,XREAL_1:10;
      then A39: dist(bb1,bb2)>=0 & r<=dK/(dK+1) by A31,XXREAL_0:2;
      conv@S2 c=|.BCS C.| by A35,SIMPLEX1:5;
      then dist(bb1,bb2)<=diameter US by A19,A26,A38,A37,A34,TBSP_1:def 8;
      then A40: dist(bb1,bb2)<=diameter K by A24,XXREAL_0:2;
      dist(x,y)=|.x-y.| by EUCLID:def 6
       .=|.X-Y.|
       .=|.r*(bb1-bb2).| by A29
       .=abs(r)*|.bb1-bb2.| by EUCLID:11
       .=r*|.bb1-bb2.| by A30,ABSVALUE:def 1
       .=r*dist(bb1,bb2) by EUCLID:def 6;
      hence dist(x,y)<=dK/(dK+1)*diameter K by A30,A40,A39,XREAL_1:66;
     end;
     hence thesis by A4,A16,TBSP_1:def 8;
    end;
   end;
  end;
  hence thesis by Def4;
 end;

theorem Th17:
  for K be bounded finite-degree non void SimplicialComplex of TOP-REAL n st
      |.K.| c= [#]K
    holds diameter BCS(k,K) <= (degree K/(degree K+1))|^k * diameter K
  proof
  let K be bounded finite-degree non void SimplicialComplex of TOP-REAL n;
  set dK=degree K;
  set ddK=dK/(dK+1);
  defpred P[Nat] means
   diameter BCS($1,K)<=ddK|^$1*diameter K & BCS($1,K) is finite-degree & degree
BCS($1,K)<=dK;
  assume A1: |.K.|c=[#]K;
  A2: for k st P[k] holds P[k+1]
  proof
   let k;
   set T=TOP-REAL n;
   set B=BCS(k,K);
   set cM=center_of_mass T;
   A3: degree K>=-1 by SIMPLEX0:23;
   assume A4: P[k];
   then reconsider B=BCS(k,K) as bounded finite-degree non void
SimplicialComplex of TOP-REAL n;
   set dB=degree B;
   A5: degree B>=-1 by SIMPLEX0:23;
   A6: 0<=diameter K by Th7;
   A7: 0<=diameter B by Th7;
   A8: |.B.|=|.K.| & [#]B=[#]K by A1,SIMPLEX1:18,19;
   then A9: BCS B=subdivision(cM,B) by A1,SIMPLEX1:def 5;
   A10: BCS(k+1,K)=BCS B by A1,SIMPLEX1:20;
   then A11: diameter BCS(k+1,K)<=dB/(dB+1)*diameter B by A1,A8,Th16;
   not{} in dom cM by ORDERS_1:1;
   then dom cM is with_non-empty_elements by SETFAM_1:def 8;
   then A12: degree BCS(k+1,K)<=dB by A9,A10,SIMPLEX0:52;
   per cases;
   suppose dB=-1 or dB=0;
    then A13: dB/(dB+1)=0;
    per cases;
    suppose dK=0 or dK=-1;
     then dK/(dK+1)=0;
     then 0=(dK/(dK+1))|^(k+1) by NAT_1:11,NEWTON:11;
     hence thesis by A1,A4,A9,A11,A12,A13,SIMPLEX1:20,XXREAL_0:2;
    end;
    suppose A14: dK<>0 & dK<>-1;
     then dK>-1 by A3,XXREAL_0:1;
     then dK>=-1+1 by INT_1:7;
     then ddK>0 by A14,XREAL_1:139;
     then ddK|^(k+1)>0 by NEWTON:83;
     hence thesis by A1,A4,A6,A9,A11,A12,A13,SIMPLEX1:20,XXREAL_0:2;
    end;
   end;
   suppose dB<>-1 & dB<>0;
    then dB>-1 by A5,XXREAL_0:1;
    then A15: dB>=-1+1 by INT_1:7;
    A16: dB/(dB+1)=(dB+1)/(dB+1)-(1/(dB+1))
     .=1-(1/(dB+1)) by A15,XCMPLX_1:60;
    A17: ddK=(dK+1)/(dK+1)-(1/(dK+1))
     .=1-(1/(dK+1)) by A4,A15,XCMPLX_1:60;
    dB+1<=dK+1 by A4,XREAL_1:6;
    then 1/(dK+1)<=1/(dB+1) by A15,XREAL_1:85;
    then degree B/(degree B+1)<=dK/(dK+1) by A16,A17,XREAL_1:10;
    then A18: degree B/(degree B+1)*diameter B<=dK/(dK+1)*((dK/(dK+1))|^k*
diameter K) by A4,A7,A15,XREAL_1:66;
    dK/(dK+1)*((dK/(dK+1))|^k*diameter K)=dK/(dK+1)*(dK/(dK+1))|^k*(diameter K)
     .=(dK/(dK+1))|^(k+1)*(diameter K) by NEWTON:6;
    hence thesis by A1,A4,A9,A11,A12,A18,SIMPLEX1:20,XXREAL_0:2;
   end;
  end;
  ddK|^(0 qua Nat)=1 by NEWTON:4;
  then A19: P[0] by A1,SIMPLEX1:16;
  for k holds P[k] from NAT_1:sch 2(A19,A2);
  hence thesis;
 end;

theorem Th18:
  for K be bounded finite-degree non void SimplicialComplex of TOP-REAL n st
      |.K.| c= [#]K for r st r>0 ex k st diameter BCS(k,K) < r
 proof
  let K be bounded finite-degree non void SimplicialComplex of TOP-REAL n such
that
   A1: |.K.|c=[#]K;
  set dK=degree K;
  let r be real number such that
   A2: r>0;
  set ddK=dK/(dK+1);
  per cases;
  suppose dK=0 or dK=-1;
   then A3: ddK=0;
   diameter BCS K<=ddK*diameter K & BCS K=BCS(1,K) by A1,Th16,SIMPLEX1:17;
   hence thesis by A2,A3;
  end;
  suppose A4: diameter K=0;
   K=BCS(0,K) by A1,SIMPLEX1:16;
   hence thesis by A2,A4;
  end;
  suppose A5: dK<>0 & dK<>-1 & diameter K<>0;
   dK>=-1 by SIMPLEX0:23;
   then dK>-1 by A5,XXREAL_0:1;
   then A6: dK>=-1+1 by INT_1:7;
   then A7: ddK>0 by A5,XREAL_1:139;
   dK+1>dK by XREAL_1:29;
   then A8: ddK<1 by A6,XREAL_1:189;
   A9: ddK in REAL & r/diameter K in REAL by XREAL_0:def 1;
   A10: diameter K>0 by A5,Th7;
   then r/diameter K>0 by A2,XREAL_1:139;
   then consider k be Element of NAT such that
    A11: ddK to_power k<r/diameter K by A7,A8,A9,TBSP_1:3;
   A12: r/diameter K*diameter K=r by A5,XCMPLX_1:87;
   A13: diameter BCS(k,K)<=ddK|^k*diameter K by A1,Th17;
   ddK to_power k=ddK|^k by POWER:41;
   then ddK|^k*diameter K<r by A10,A11,A12,XREAL_1:68;
   then diameter BCS(k,K)<r by A13,XXREAL_0:2;
   hence thesis;
  end;
 end;

theorem Th19:
  for i,j be Element of NAT
  ex f be Function of[:TOP-REAL i,TOP-REAL j:],TOP-REAL(i+j) st
    f is being_homeomorphism &
    for fi be Element of TOP-REAL i,fj be Element of TOP-REAL j
    holds f.(fi,fj) = fi^fj
 proof
  let i,j be Element of NAT;
  set TRi=TOP-REAL i,TRj=TOP-REAL j,TRij=TOP-REAL(i+j);
  set tri=the TopStruct of TRi,trj=the TopStruct of TRj,trij=the TopStruct of
TRij;
  A1: trj=TopSpaceMetr Euclid j by EUCLID:def 8;
  trij=TopSpaceMetr Euclid(i+j) & tri=TopSpaceMetr Euclid i by EUCLID:def 8;
  then consider f be Function of[:tri,trj:],trij such that
   A2: f is being_homeomorphism and
   A3: for fi,fj be FinSequence st[fi,fj] in dom f holds f.(fi,fj)=fi^fj by A1,
TOPREAL7:26;
  rng f=[#]trij by A2,TOPS_2:60;
  then A4: rng f=[#]TRij;
  A5: [#][:TRi,TRj:]=[:[#]TRi,[#]TRj:] by BORSUK_1:def 2;
  A6: [:TRi,TRj:]=[:TRi,TRj:]|([#][:TRi,TRj:]) by TSEP_1:3
   .=[:TRi|([#]TRi),TRj|([#]TRj):] by A5,BORSUK_3:22
   .=[:tri,TRj|([#]TRj):] by TSEP_1:93
   .=[:tri,trj:] by TSEP_1:93;
  then reconsider F=f as Function of[:TRi,TRj:],TRij;
  A7: now let P be Subset of[:TRi,TRj:];
   thus F.:(Cl P)=Cl(f.:P) by A2,A6,TOPS_2:60
    .=Cl(F.:P) by TOPS_3:80;
  end;
  take F;
  A8: F is one-to-one by A2,TOPS_2:60;
  dom F=[#][:TRi,TRj:] by A2,A6,TOPS_2:60;
  hence F is being_homeomorphism by A4,A7,A8,TOPS_2:60;
  let fi be Element of TOP-REAL i,fj be Element of TOP-REAL j;
  dom F=[:[#]TRi,[#]TRj:] by A5,FUNCT_2:def 1;
  then [fi,fj] in dom F by ZFMISC_1:87;
  hence thesis by A3;
 end;

Lm4: for n be Nat holds [#]TOP-REAL n=[#]TopSpaceMetr Euclid n
 proof
  let n be Nat;
  the TopStruct of TOP-REAL n=TopSpaceMetr Euclid n by EUCLID:def 8;
  hence thesis;
 end;

theorem Th20:
  for i,j be Element of NAT
  for f be Function of [:TOP-REAL i,TOP-REAL j:],TOP-REAL(i+j) st
       for fi be Element of TOP-REAL i,fj be Element of TOP-REAL j
         holds f.(fi,fj) = fi^fj
  for r for fi be Point of Euclid i,fj be Point of Euclid j,
            fij be Point of Euclid(i+j) st fij = fi^fj
    holds f.:[:OpenHypercube(fi,r),OpenHypercube(fj,r):] = OpenHypercube(fij,r)
  proof
  let i,j be Element of NAT;
  let f be Function of[:TOP-REAL i,TOP-REAL j:],TOP-REAL(i+j) such that
   A1: for fi be Element of TOP-REAL i,fj be Element of TOP-REAL j holds f.(fi,
fj)=fi^fj;
  let r be real number,fi be Point of Euclid i,fj be Point of Euclid j,fij be
Point of Euclid(i+j) such that
   A2: fij=fi^fj;
  set Ii=Intervals(fi,r),Ij=Intervals(fj,r),Iij=Intervals(fij,r);
  A3: OpenHypercube(fi,r)=product Ii by EUCLID_9:def 4;
  A4: [#]TOP-REAL i=[#]TopSpaceMetr Euclid i by Lm4;
  A5: [#]TOP-REAL j=[#]TopSpaceMetr Euclid j by Lm4;
  A6: OpenHypercube(fj,r)=product Ij by EUCLID_9:def 4;
  A7: Ii^Ij=Iij by A2,RLAFFIN3:1;
  A8: f.:[:product Ii,product Ij:]c=product Iij
  proof
   let y be set;
   assume y in f.:[:product Ii,product Ij:];
   then consider x be set such that
    x in dom f and
    A9: x in [:product Ii,product Ij:] and
    A10: f.x=y by FUNCT_1:def 6;
   consider xi,xj be set such that
    A11: xi in product Ii and
    A12: xj in product Ij and
    A13: x=[xi,xj] by A9,ZFMISC_1:def 2;
   reconsider xi as Element of TOP-REAL i by A3,A4,A11;
   reconsider xj as Element of TOP-REAL j by A5,A6,A12;
   y=f.(xi,xj) by A10,A13,BINOP_1:def 1
    .=xi^xj by A1;
   hence y in product Iij by A7,A11,A12,RLAFFIN3:2;
  end;
  A14: product Iij c=f.:[:product Ii,product Ij:]
  proof
   let y be set;
   assume y in product Iij;
   then consider p1,p2 be FinSequence such that
    A15: y=p1^p2 and
    A16: p1 in product Ii & p2 in product Ij by A7,RLAFFIN3:2;
   A17: [p1,p2] in [:product Ii,product Ij:] by A16,ZFMISC_1:87;
   [p1,p2] in [:[#]TOP-REAL i,[#]TOP-REAL j:] by A3,A5,A4,A6,A16,ZFMISC_1:87;
   then [p1,p2] in [#][:TOP-REAL i,TOP-REAL j:];
   then A18: [p1,p2] in dom f by FUNCT_2:def 1;
   y=f.(p1,p2) by A1,A3,A5,A4,A6,A15,A16
    .=f. [p1,p2] by BINOP_1:def 1;
   hence thesis by A17,A18,FUNCT_1:def 6;
  end;
  OpenHypercube(fij,r)=product Iij by EUCLID_9:def 4;
  hence thesis by A3,A6,A8,A14,XBOOLE_0:def 10;
 end;

theorem Th21:
  A is bounded iff ex p be Point of Euclid n,r st A c= OpenHypercube(p,r)
 proof
  reconsider B=A as Subset of Euclid n by TOPREAL3:8;
  thus A is bounded implies ex p be Point of Euclid n,r be real number st A c=
OpenHypercube(p,r)
  proof
   assume A is bounded;
   then A1: B is bounded by JORDAN2C:11;
   per cases;
   suppose A2: A is empty;
    take p=the Point of Euclid n,r=the real number;
    thus thesis by A2,XBOOLE_1:2;
   end;
   suppose A is non empty;
    then consider p be set such that
     A3: p in B by XBOOLE_0:def 1;
    reconsider p as Element of Euclid n by A3;
    consider r be Real such that
     0<r and
     A4: for x,y being Point of Euclid n st x in B & y in B holds dist(x,y)<=r
by A1,TBSP_1:def 7;
    take p,r1=r+1;
    A5: B c=Ball(p,r1)
    proof
     let x be set;
     assume A6: x in B;
     then reconsider x as Element of Euclid n;
     dist(p,x)<r1 by A3,A4,A6,XREAL_1:39;
     hence thesis by METRIC_1:11;
    end;
    Ball(p,r1)c=OpenHypercube(p,r1) by EUCLID_9:22;
    hence A c=OpenHypercube(p,r1) by A5,XBOOLE_1:1;
   end;
  end;
  given p be Point of Euclid n,r be real number such that
   A7: A c= OpenHypercube(p,r);
  per cases;
  suppose n=0; then
   OpenHypercube(p,r) = {{}} by EUCLID_9:12; then
   B = {} or B = {0} by A7,ZFMISC_1:33;
   hence thesis by JORDAN2C:11;
  end;
  suppose n<>0;
   then OpenHypercube(p,r)c=Ball(p,r*sqrt(n)) by EUCLID_9:18;
   then B is bounded by A7,TBSP_1:14,XBOOLE_1:1;
   hence thesis by JORDAN2C:11;
  end;
 end;

Lm5: for A be Subset of TOP-REAL 1 holds A is closed & A is bounded implies A
is compact
 proof
  set TR1=TOP-REAL 1;
  let A be Subset of TR1 such that
   A1: A is closed and
   A2: A is bounded;
  consider r be Real such that
   A3: for q be Point of TR1 st q in A holds|.q.|<r by A2,JORDAN2C:34;
  reconsider L=[.-r,r.] as Subset of R^1 by TOPMETR:17;
  consider f be Function of TR1,R^1 such that
   A4: for p be Element of TR1 holds f.p=p/.1 by JORDAN2B:1;
  A5: f is being_homeomorphism by A4,JORDAN2B:28;
  then reconsider F=f as one-to-one Function by TOPS_2:def 5;
  rng f=[#]R^1 by A5,TOPS_2:def 5;
  then f is onto by FUNCT_2:def 3;
  then f/"=F" by TOPS_2:def 4;
  then A6: (f/").:L=F"L by FUNCT_1:85;
  A7: dom f=[#]TR1 by A5,TOPS_2:def 5;
  A8: A c=F"L
  proof
   let x be set;
   assume A9: x in A;
   then reconsider v=x as Element of TR1;
   set v1=v.1;
   A10: len v=1 by CARD_1:def 7;
   then v=<*v1*> by FINSEQ_1:40;
   then A11: |.v.|=abs v1 by TOPREALC:18;
   |.v.|<r by A3,A9;
   then v1<=r & -r<=v1 by A11,ABSVALUE:5;
   then A12: v1 in L by XXREAL_1:1;
   1 in Seg 1 & dom v=Seg 1 by A10,FINSEQ_1:1,def 3;
   then A13: v/.1=v1 by PARTFUN1:def 6;
   f.v=v/.1 by A4;
   hence thesis by A7,A12,A13,FUNCT_1:def 7;
  end;
  [.-r,r.] is compact by RCOMP_1:6;
  then A14: L is compact by JORDAN5A:25;
  f" is continuous by A5,TOPS_2:def 5;
  then (f/").:L is compact by A14,WEIERSTR:8;
  hence thesis by A1,A6,A8,COMPTS_1:9;
 end;

Lm6: for A be Subset of TOP-REAL n holds A is closed & A is bounded implies A
is compact
 proof
  defpred P[Nat] means
   for A be Subset of TOP-REAL$1 holds A is closed & A is bounded implies A is
compact;
  A1: for n be Nat st P[n] holds P[n+1]
  proof
   let n be Nat such that
    A2: P[n];
   per cases;
   suppose n=0;
    hence thesis by Lm5;
   end;
   suppose A3: n<>0;
    set n1=n+1;
    set TR1=TOP-REAL 1;
    set TRn=TOP-REAL n;
    set TRn1=TOP-REAL n1;
    let A be Subset of TRn1;
    assume that
     A4: A is closed and
     A5: A is bounded;
    consider p be Point of Euclid n1,r be real number such that
     A6: A c=OpenHypercube(p,r) by A5,Th21;
    A7: n in NAT by ORDINAL1:def 12;
    then consider f be Function of[:TRn,TR1:],TRn1 such that
     A8: f is being_homeomorphism and
     A9: for fi be Element of TRn,fj be Element of TR1 holds f.(fi,fj)=fi^fj
by Th19;
    A10: f is one-to-one & dom f=[#][:TRn,TR1:] by A8,TOPGRP_1:24;
    len p=n1 by CARD_1:def 7;
    then consider q1,q2 be FinSequence such that
     A11: len q1=n and
     A12: len q2=1 and
     A13: p=q1^q2 by FINSEQ_2:22;
    rng p c=REAL;
    then A14: p is FinSequence of REAL by FINSEQ_1:def 4;
    then A15: q1 is FinSequence of REAL by A13,FINSEQ_1:36;
    A16: q2 is FinSequence of REAL by A13,A14,FINSEQ_1:36;
    reconsider q1 as Element of Euclid n by A11,A15,TOPREAL3:45;
    reconsider q2 as Element of Euclid 1 by A12,A16,TOPREAL3:45;
    A17: f is continuous by A8,TOPS_2:def 5;
    reconsider Bn=cl_Ball(q1,r*sqrt(n)) as Subset of TRn by TOPREAL3:8;
    reconsider B1=cl_Ball(q2,r*sqrt(1)) as Subset of TR1 by TOPREAL3:8;
    Ball(q2,r*sqrt(1))c=B1 & OpenHypercube(q2,r)c=Ball(q2,r*sqrt(1)) by
EUCLID_9:18,METRIC_1:14;
    then A18: OpenHypercube(q2,r)c=B1 by XBOOLE_1:1;
    Ball(q1,r*sqrt(n))c=Bn & OpenHypercube(q1,r)c=Ball(q1,r*sqrt(n)) by A3,
EUCLID_9:18,METRIC_1:14;
    then OpenHypercube(q1,r)c=Bn by XBOOLE_1:1;
    then A19: [:OpenHypercube(q1,r),OpenHypercube(q2,r):]c=[:Bn,B1:] by A18,
ZFMISC_1:96;
    cl_Ball(q2,r*sqrt(1)) is bounded by TOPREAL6:59;
    then B1 is bounded by JORDAN2C:11;
    then A20: B1 is compact by Lm5,TOPREAL6:58;
    cl_Ball(q1,r*sqrt(n)) is bounded by TOPREAL6:59;
    then Bn is bounded by JORDAN2C:11;
    then Bn is compact by A2,A7,TOPREAL6:58;
    then A21: [:Bn,B1:] is compact Subset of[:TRn,TR1:] by A20,BORSUK_3:23;
    rng f=[#]TRn1 by A8,TOPGRP_1:24;
    then A22: f.:(f"A)=A by FUNCT_1:77;
    f.:[:OpenHypercube(q1,r),OpenHypercube(q2,r):]=OpenHypercube(p,r) by A9,A11
,A13,Th20;
    then A23: f"A c=[:OpenHypercube(q1,r),OpenHypercube(q2,r):] by A6,A10,A22,
FUNCT_1:87;
    f"A is closed by A4,A8,TOPGRP_1:24;
    then f"A is compact by A19,A21,A23,COMPTS_1:9,XBOOLE_1:1;
    hence thesis by A17,A22,WEIERSTR:8;
   end;
  end;
  A24: P[0];
  for n holds P[n] from NAT_1:sch 2(A24,A1);
  hence thesis;
 end;

registration
 let n;
 cluster closed bounded -> compact for Subset of TOP-REAL n;
 coherence by Lm6;
end;

registration
 let n;
 let A be affinely-independent Subset of TOP-REAL n;
 cluster conv A -> compact;
 coherence
 proof
  n in NAT by ORDINAL1:def 12;
  then conv A is bounded by Th14;
  hence thesis;
 end;
end;

begin :: Main Theorems

theorem Th22:
  for A be non empty affinely-independent Subset of TOP-REAL n
  for E be Enumeration of A
  for F be FinSequence of bool the carrier of ((TOP-REAL n)|(conv A)) st
    len F = card A & rng F is closed &
    for S be Subset of dom F holds conv(E.:S) c= union(F.:S)
      holds meet rng F is non empty
 proof
  set TRn=TOP-REAL n;
  let A be non empty affinely-independent Subset of TRn;
  set cA=conv A;
  let E be Enumeration of A;
  let F be FinSequence of bool the carrier of(TRn|cA) such that
   A1: len F=card A and
   A2: rng F is closed and
   A3: for S be Subset of dom F holds conv(E.:S)c=union(F.:S);
  A4: F<>{} by A1;
  A5: rng E=A by RLAFFIN3:def 1;
  then len E=card A by FINSEQ_4:62;
  then A6: dom E=dom F by A1,FINSEQ_3:29;
  set En=Euclid n;
  set Comp=Complex_of{A};
  defpred P[set,set] means
   $1 in F.(E".$2) & for B be Subset of TRn st B c=A & $1 in conv B holds$2 in
B;
  A7: TopSpaceMetr En=the TopStruct of TRn by EUCLID:def 8;
  then reconsider CA=cA as non empty Subset of TopSpaceMetr En;
  reconsider ca=cA as non empty Subset of En by A7;
  A8: (TopSpaceMetr En)|CA=TopSpaceMetr(En|ca) by HAUSDORF:16;
  then reconsider CrF=COMPLEMENT(rng F) as Subset-Family of TopSpaceMetr(En|ca)
by A7,PRE_TOPC:36;
  CA is compact by A7,COMPTS_1:23;
  then A9: TopSpaceMetr(En|ca) is compact by A8,COMPTS_1:3;
  A10: (TopSpaceMetr En)|CA=TRn|cA by A7,PRE_TOPC:36;
  assume meet rng F is empty;
  then [#](TRn|cA)=(meet rng F)`
   .=union CrF by A4,TOPS_2:7;
  then A11: CrF is Cover of TopSpaceMetr(En|ca) by A8,A10,SETFAM_1:45;
  set L=the Lebesgue_number of CrF;
  A12: |.Comp.|c=[#]Comp;
  then consider k be Nat such that
   A13: diameter BCS(k,Comp)<L by Th18;
  set Bcs=BCS(k,Comp);
  A14: |.Bcs.|=|.Comp.| by A12,SIMPLEX1:19;
  A15: the topology of Comp=bool A by SIMPLEX0:4;
  A16: for x be set st x in Vertices Bcs ex y be set st y in A & P[x,y]
  proof
   let x be set;
   assume A17: x in Vertices Bcs;
   then reconsider v=x as Element of Bcs;
   v is vertex-like by A17,SIMPLEX0:def 4;
   then consider S be Subset of Bcs such that
    A18: S is simplex-like and
    A19: v in S by SIMPLEX0:def 3;
   @S c=conv@S by RLAFFIN1:2;
   then A20: v in conv@S by A19;
   conv@S c=|.Comp.| by A14,A18,SIMPLEX1:5;
   then consider W be Subset of Comp such that
    A21: W is simplex-like and
    A22: v in Int@W by A20,SIMPLEX1:6;
   A23: v in conv@W by A22,RLAFFIN2:def 1;
   A24: W in the topology of Comp by A21,PRE_TOPC:def 2;
   then E"W c=dom E & E.:(E"W)=W by A5,A15,FUNCT_1:77,RELAT_1:132;
   then conv@W c=union(F.:(E"W)) by A3,A6;
   then consider Y be set such that
    A25: v in Y and
    A26: Y in F.:(E"W) by A23,TARSKI:def 4;
   consider i be set such that
    i in dom F and
    A27: i in E"W and
    A28: F.i=Y by A26,FUNCT_1:def 6;
   take y=E.i;
   A29: y in W by A27,FUNCT_1:def 7;
   i in dom E by A27,FUNCT_1:def 7;
   hence y in A & x in F.(E".y) by A15,A24,A25,A28,A29,FUNCT_1:34;
   let B be Subset of TRn;
   assume that
    A30: B c=A and
    A31: x in conv B;
   reconsider b=B as Simplex of Comp by A15,A30,PRE_TOPC:def 2;
   conv@b meets Int@W by A22,A31,XBOOLE_0:3;
   then W c=b by A21,SIMPLEX1:26;
   hence thesis by A29;
  end;
  consider G be Function of Vertices Bcs,A such that
   A32: for x be set st x in Vertices Bcs holds P[x,G.x] from FUNCT_2:sch 1(A16
);
  A33: |.Comp.|=conv A by SIMPLEX1:8;
  then Bcs is with_non-empty_element by A14,SIMPLEX1:7;
  then for v be Vertex of Bcs,B be Subset of TRn st B c=A & v in conv B holds G
.v in B by A32;
  then consider S be Simplex of card A-1,Bcs such that
   A34: G.:S=A by SIMPLEX1:47;
  A35: [#]Bcs=[#]Comp by A12,SIMPLEX1:18;
  then reconsider SS=S as Subset of En by A7;
  S is non empty by A34;
  then consider s be set such that
   A36: s in S by XBOOLE_0:def 1;
  A37: conv@S c=cA by A14,A33,SIMPLEX1:5;
  reconsider s as Point of En by A7,A35,A36;
  A38: S c=conv@S by RLAFFIN1:2;
  then s in conv@S by A36;
  then reconsider ss=s as Point of En|ca by A37,TOPMETR:def 2;
  A39: SS is bounded;
  CrF is open by A2,A8,A10,TOPS_2:9;
  then consider CRF be Subset of TopSpaceMetr(En|ca) such that
   A40: CRF in CrF and
   A41: Ball(ss,L)c=CRF by A9,A11,Def1;
  CRF` in rng F by A8,A10,A40,SETFAM_1:def 7;
  then consider i be set such that
   A42: i in dom F and
   A43: F.i=CRF` by FUNCT_1:def 3;
  E.i in A by A5,A6,A42,FUNCT_1:def 3;
  then consider w be set such that
   A44: w in dom G and
   A45: w in S and
   A46: G.w=E.i by A34,FUNCT_1:def 6;
  A47: w in conv@S by A38,A45;
  A48: conv@S c=cA by A14,A33,SIMPLEX1:5;
  then A49: [#](En|ca)=ca & w in cA by A47,TOPMETR:def 2;
  reconsider SS=S as bounded Subset of En by A39;
  diameter SS<=diameter BCS(k,Comp) by Def4;
  then A50: diameter SS<L by A13,XXREAL_0:2;
  w in F.(E".(G.w)) by A32,A44;
  then A51: w in F.i by A6,A42,A46,FUNCT_1:34;
  reconsider w as Point of En by A49;
  reconsider ww=w as Point of En|ca by A47,A48,TOPMETR:def 2;
  conv@S c=cl_Ball(s,diameter SS) by A36,A38,Th13;
  then dist(s,w)=dist(ss,ww) & dist(s,w)<=diameter SS by A47,METRIC_1:12
,TOPMETR:def 1;
  then dist(ss,ww)<L by A50,XXREAL_0:2;
  then ww in Ball(ss,L) by METRIC_1:11;
  hence contradiction by A41,A43,A51,XBOOLE_0:def 5;
 end;

reserve A for affinely-independent Subset of TOP-REAL n;

theorem Th23:
  for A st card A = n+1
  for f be continuous Function of(TOP-REAL n)|conv A,(TOP-REAL n)|conv A
  ex p be Point of TOP-REAL n st p in dom f & f.p=p
  proof
  set TRn=TOP-REAL n;
  let A be affinely-independent Subset of TRn such that
   A1: card A=n+1;
  A2: A is non empty by A1;
  set cA=conv A;
  let f be continuous Function of TRn|cA,TRn|cA;
  reconsider cA as non empty Subset of TRn by A2;
  set T=TRn|cA;
  reconsider ff=f as continuous Function of T,T;
  set E=the Enumeration of A;
  deffunc P(set)={v where v is Element of T: |--(A,E.$1).(f.v)<=|--(A,E.$1).v};
  consider F be FinSequence such that
   A3: len F=card A & for k st k in dom F holds F.k=P(k) from FINSEQ_1:sch 2;
  rng F c=bool the carrier of T
  proof
   let y be set;
   assume y in rng F;
   then consider x be set such that
    A4: x in dom F and
    A5: F.x=y by FUNCT_1:def 3;
   A6: P(x)c=the carrier of T
   proof
    let z be set;
    assume z in P(x);
    then ex v be Element of T st z=v & |--(A,E.x).(f.v)<=|--(A,E.x).v;
    hence thesis;
   end;
   F.x=P(x) by A3,A4;
   hence thesis by A5,A6;
  end;
  then reconsider F as FinSequence of bool the carrier of T by FINSEQ_1:def 4;
  A7: [#]T=cA by PRE_TOPC:def 5;
  A8: dom f=the carrier of T by FUNCT_2:def 1;
  now let W be Subset of T;
   reconsider Z=0 as real number;
   reconsider L=].-infty,Z.] as Subset of R^1 by TOPMETR:17;
   assume W in rng F;
   then consider i be set such that
    A9: i in dom F and
    A10: F.i=W by FUNCT_1:def 3;
   reconsider AEi=|--(A,E.i) as continuous Function of TRn,R^1 by A1,
RLAFFIN3:32;
   set AT=AEi|T;
   set Af=AT*ff;
   set AfT=Af-AT;
   A11: dom AfT=the carrier of T by FUNCT_2:def 1;
   reconsider AfT as Function of T,R^1 by TOPMETR:17;
   A12: dom AT=the carrier of T by FUNCT_2:def 1;
   A13: AT=AEi|the carrier of T by A7,TMAP_1:def 3;
   A14: dom Af=the carrier of T by FUNCT_2:def 1;
   A15: AfT"L c=P(i)
   proof
    let x be set;
    assume A16: x in AfT"L;
    then reconsider v=x as Point of T;
    x in dom AfT by A16,FUNCT_1:def 7;
    then A17: AfT.x=Af.x-AT.x by VALUED_1:13;
    AfT.x in L & Af.x=AT.(f.x) by A14,A16,FUNCT_1:12,def 7;
    then AT.(f.x)-AT.x<=0 by A17,XXREAL_1:2;
    then A18: AT.(f.x)<=AT.x by XREAL_1:50;
    f.x in dom AT by A14,A16,FUNCT_1:11;
    then A19: AT.(f.x)=AEi.(f.v) by A13,FUNCT_1:47;
    AT.x=AEi.v by A12,A13,FUNCT_1:47;
    hence thesis by A18,A19;
   end;
   A20: P(i)c=AfT"L
   proof
    let x be set;
    assume x in P(i);
    then consider v be Element of T such that
     A21: x=v and
     A22: AEi.(f.v)<=AEi.v;
    f.v in rng f by A8,FUNCT_1:def 3;
    then A23: AEi.(f.v)=AT.(f.v) by A12,A13,FUNCT_1:47;
    AEi.v=AT.v by A12,A13,FUNCT_1:47;
    then Af.v<=AT.v by A14,A22,A23,FUNCT_1:12;
    then Af.v-AT.v<=0 by XREAL_1:47;
    then AfT.v<=0 by A11,VALUED_1:13;
    then AfT.v in L by XXREAL_1:234;
    hence thesis by A11,A21,FUNCT_1:def 7;
   end;
   L is closed by BORSUK_5:41;
   then A24: AfT"L is closed by PRE_TOPC:def 6;
   F.i=P(i) by A3,A9;
   hence W is closed by A10,A15,A20,A24,XBOOLE_0:def 10;
  end;
  then A25: rng F is closed by TOPS_2:def 2;
  A26: dom E=Seg len E by FINSEQ_1:def 3;
  A27: conv A c=Affin A by RLAFFIN1:65;
  A28: rng E=A by RLAFFIN3:def 1;
  then len E=card A by FINSEQ_4:62;
  then A29: dom F=dom E by A3,FINSEQ_3:29;
  for S be Subset of dom F holds conv(E.:S)c=union(F.:S)
  proof
   let S be Subset of dom F;
   set ES=E.:S;
   per cases;
   suppose S is empty;
    then conv ES is empty;
    hence thesis by XBOOLE_1:2;
   end;
   suppose A30: S is non empty;
    let x be set;
    set fx=f.x,xES=x|--ES,fxA=fx|--A,xA=x|--A;
    assume A31: x in conv ES;
    A32: conv ES c=conv A by A28,RELAT_1:111,RLAFFIN1:3;
    then reconsider v=x as Point of T by A7,A31;
    A33: len(fxA*E)=len E by FINSEQ_2:33;
    A34: len E=len(xES*E) by FINSEQ_2:33;
    then reconsider fxAE=fxA*E,xESE=xES*E as Element of len E-tuples_on REAL
by A33,FINSEQ_2:92;
    A35: dom fxAE=Seg len E by A33,FINSEQ_1:def 3;
    A36: conv ES c=Affin ES by RLAFFIN1:65;
    then A37: xA=xES by A28,A31,RELAT_1:111,RLAFFIN1:77;
    A38: ES c=A by A28,RELAT_1:111;
    A39: Carrier xES c=ES by RLVECT_2:def 6;
    ES is affinely-independent by A28,RELAT_1:111,RLAFFIN1:43;
    then sum xES=1 & Carrier xES c= A by A31,A36,A38,A39,RLAFFIN1:def 7
,XBOOLE_1:1;
    then A40: Carrier fxA c=A & 1=Sum(xES*E) by A28,RLAFFIN1:30,RLVECT_2:def 6;
    A41: fx in rng f by A7,A8,A31,A32,FUNCT_1:def 3;
    then A42: fx in conv A by A7;
    then sum fxA=1 by A27,RLAFFIN1:def 7;
    then A43: Sum fxAE=Sum xESE by A28,A40,RLAFFIN1:30;
    A44: dom xESE=Seg len E by A34,FINSEQ_1:def 3;
    per cases by A43,RVSUM_1:83;
    suppose ex j be Nat st j in Seg len E & fxAE.j<xESE.j;
     then consider j be Nat such that
      A45: j in Seg len E and
      A46: fxAE.j<xESE.j;
     A47: fxAE.j=fxA.(E.j) by A35,A45,FUNCT_1:12;
     A48: xESE.j=xES.(E.j) by A44,A45,FUNCT_1:12;
     then xESE.j=|--(A,E.j).x by A31,A37,RLAFFIN3:def 3;
     then A49: |--(A,E.j).(f.v)<=|--(A,E.j).v by A42,A46,A47,RLAFFIN3:def 3;
     A50: E.j in dom fxA by A35,A45,FUNCT_1:11;
     then 0<xES.(E.j) by A7,A41,A46,A47,A48,RLAFFIN1:71;
     then E.j in Carrier xES by A50,RLVECT_2:19;
     then consider i be set such that
      A51: i in dom E and
      A52: i in S and
      A53: E.i=E.j by A39,FUNCT_1:def 6;
     i=j by A26,A45,A51,A53,FUNCT_1:def 4;
     then A54: F.j in F.:S by A52,FUNCT_1:def 6;
     P(j)=F.j by A3,A26,A29,A45;
     then x in F.j by A49;
     hence thesis by A54,TARSKI:def 4;
    end;
    suppose A55: for j be Nat st j in Seg len E holds fxAE.j<=xESE.j;
     consider j be set such that
      A56: j in S by A30,XBOOLE_0:def 1;
     reconsider j as Nat by A56;
     A57: fxAE.j<=xESE.j by A26,A29,A55,A56;
     A58: P(j)=F.j by A3,A56;
     xESE.j=xES.(E.j) by A26,A29,A44,A56,FUNCT_1:12;
     then A59: xESE.j=|--(A,E.j).x by A31,A37,RLAFFIN3:def 3;
     fxAE.j=fxA.(E.j) by A26,A29,A35,A56,FUNCT_1:12;
     then |--(A,E.j).(f.v)<=|--(A,E.j).v by A42,A59,A57,RLAFFIN3:def 3;
     then A60: x in F.j by A58;
     F.j in F.:S by A56,FUNCT_1:def 6;
     hence thesis by A60,TARSKI:def 4;
    end;
   end;
  end;
  then meet rng F is non empty by A2,A3,A25,Th22;
  then consider v be set such that
   A61: v in meet rng F by XBOOLE_0:def 1;
  A62: v in cA by A7,A61;
  then reconsider v as Element of TRn;
  set fv=f.v,vA=v|--A,fvA=fv|--A;
  A63: len(fvA*E)=len E by FINSEQ_2:33;
  fv in rng f by A8,A61,FUNCT_1:def 3;
  then A64: fv in cA by A7;
  then Carrier fvA c=A & sum fvA=1 by A27,RLAFFIN1:def 7,RLVECT_2:def 6;
  then A65: Carrier vA c=A & 1=Sum(fvA*E) by A28,RLAFFIN1:30,RLVECT_2:def 6;
  A66: len E=len(vA*E) by FINSEQ_2:33;
  then reconsider fvAE=fvA*E,vAE=vA*E as Element of len E-tuples_on REAL by A63
,FINSEQ_2:92;
  A67: dom fvAE=Seg len E by A63,FINSEQ_1:def 3;
  A68: dom vAE=Seg len E by A66,FINSEQ_1:def 3;
  A69: for j be Nat st j in Seg len E holds fvAE.j<=vAE.j
  proof
   let j be Nat;
   assume A70: j in Seg len E;
   then F.j=P(j) & F.j in rng F by A3,A26,A29,FUNCT_1:def 3;
   then v in P(j) by A61,SETFAM_1:def 1;
   then A71: ex w be Element of T st w=v & |--(A,E.j).(f.w)<=|--(A,E.j).w;
   A72: |--(A,E.j).v=vA.(E.j) by RLAFFIN3:def 3
    .=vAE.j by A68,A70,FUNCT_1:12;
   |--(A,E.j).fv=fvA.(E.j) by A64,RLAFFIN3:def 3
    .=fvAE.j by A67,A70,FUNCT_1:12;
   hence thesis by A71,A72;
  end;
  A73: Carrier vA c=A by RLVECT_2:def 6;
  sum vA=1 by A27,A62,RLAFFIN1:def 7;
  then A74: Sum fvAE=Sum vAE by A28,A65,RLAFFIN1:30;
  A75: Carrier fvA c=A by RLVECT_2:def 6;
  A76: now let w be Element of TRn;
   per cases;
   suppose w in A;
    then consider j be set such that
     A77: j in dom E and
     A78: E.j=w by A28,FUNCT_1:def 3;
    A79: fvAE.j=fvA.w & vAE.j=vA.w by A77,A78,FUNCT_1:13;
    fvAE.j<=vAE.j & fvAE.j>=vAE.j by A26,A74,A69,A77,RVSUM_1:83;
    hence vA.w=fvA.w by A79,XXREAL_0:1;
   end;
   suppose A80: not w in A;
    then not w in Carrier vA by A73;
    then A81: vA.w=0 by RLVECT_2:19;
    not w in Carrier fvA by A75,A80;
    hence vA.w=fvA.w by A81,RLVECT_2:19;
   end;
  end;
  A82: Sum vA=v by A27,A62,RLAFFIN1:def 7;
  Sum fvA=fv by A27,A64,RLAFFIN1:def 7;
  then v=fv by A76,A82,RLVECT_2:def 9;
  hence thesis by A8,A61;
 end;

theorem
  for A st card A = n+1
  for f be continuous Function of (TOP-REAL n)|conv A,(TOP-REAL n)|conv A
    holds f is with_fixpoint
 proof
  let A be affinely-independent Subset of TOP-REAL n such that
   A1: card A=n+1;
  let f be continuous Function of(TOP-REAL n)|conv A,(TOP-REAL n)|conv A;
  consider x be Point of TOP-REAL n such that
   A2: x in dom f & f.x=x by A1,Th23;
  x is_a_fixpoint_of f by A2,ABIAN:def 3;
  hence thesis by ABIAN:def 5;
 end;

theorem Th25:
  card A = n+1 implies ind conv A = n
  proof
  set TR=TOP-REAL n;
  assume A1: card A=n+1;
  set C=conv A;
  A2: ind C>=n
  proof
   set E=the Enumeration of A;
   assume A3: ind C<n;
   A is non empty by A1;
   then reconsider C as non empty Subset of TR;
   ind C is natural;
   then reconsider n1=n-1 as Nat by A3,NAT_1:20;
   deffunc F(set)=C\conv(A\{E.$1});
   reconsider c =C as Subset of the TopStruct of TR;
   set TRC=TR|C;
   set carr=the carrier of TRC;
   A4: the TopStruct of TR=TopSpaceMetr Euclid n & the TopStruct of TRC=(the
TopStruct of TR)|c by EUCLID:def 8,PRE_TOPC:36;
   consider f be FinSequence such that
    A5: len f=len E & for k st k in dom f holds f.k=F(k) from FINSEQ_1:sch 2;
   A6: [#]TRC=C by PRE_TOPC:def 5;
   rng f c=bool carr
   proof
    let y be set;
    assume y in rng f;
    then consider x be set such that
     A7: x in dom f and
     A8: f.x=y by FUNCT_1:def 3;
    f.x=F(x) by A5,A7;
    then f.x c=C by XBOOLE_1:36;
    hence thesis by A6,A8;
   end;
   then reconsider R=rng f as finite Subset-Family of TRC;
   A9: rng E=A by RLAFFIN3:def 1;
   then A10: len E=card A by FINSEQ_4:62;
   A11: dom f=dom E by A5,FINSEQ_3:29;
   the carrier of TRC c=union R
   proof
    let x be set;
    assume A12: x in the carrier of TRC;
    assume A13: not x in union R;
    now let y be set;
     assume A14: y in A;
     then consider n be set such that
      A15: n in dom E and
      A16: E.n=y by A9,FUNCT_1:def 3;
     reconsider n as Nat by A15;
     f.n=F(n) by A5,A11,A15;
     then F(n) in R by A11,A15,FUNCT_1:def 3;
     then not x in F(n) by A13,TARSKI:def 4;
     then conv(A\{E.n})c=Affin(A\{E.n}) & x in conv(A\{E.n}) by A6,A12,
RLAFFIN1:65,XBOOLE_0:def 5;
     then A17: x|--A=x|--(A\{E.n}) by RLAFFIN1:77,XBOOLE_1:36;
     Carrier(x|--(A\{E.n}))c=A\{E.n} & E.n in {E.n} by RLVECT_2:def 6
,TARSKI:def 1;
     then not E.n in Carrier(x|--(A\{E.n})) by XBOOLE_0:def 5;
     hence (x|--A).y=0 by A14,A16,A17,RLVECT_2:19;
    end;
    then A18: x in conv(A\A) by A6,A12,RLAFFIN1:76;
    A\A={} by XBOOLE_1:37;
    hence contradiction by A18;
   end;
   then A19: R is Cover of TRC by SETFAM_1:def 11;
   now let U be Subset of TRC;
    assume U in R;
    then consider x be set such that
     A20: x in dom f & f.x=U by FUNCT_1:def 3;
    reconsider cAE=conv(A\{E.x}) as Subset of TRC by A6,RLAFFIN1:3,XBOOLE_1:36
;
    A\{E.x} is affinely-independent by RLAFFIN1:43,XBOOLE_1:36;
    then A21: cAE is closed by TSEP_1:8;
    U=cAE` by A6,A5,A20;
    hence U is open by A21;
   end;
   then A22: ind TRC=ind C & R is open by TOPDIM_1:17,TOPS_2:def 1;
   ind C<n1+1 by A3;
   then ind C<=n1 by NAT_1:13;
   then consider G be finite Subset-Family of TRC such that
    A23: G is open and
    A24: G is Cover of TRC and
    A25: G is_finer_than R and
    card G<=card R*(n1+1) and
    A26: order G<=n1 by A4,A22,A19,TOPDIM_2:23;
   defpred P[Nat,set,set] means
    $3={g where g is Subset of TRC:g in G & (g c=f.($1+1) or g in $2)};
   defpred P[set] means
    $1 in G & $1c=f.1;
   consider G0 be Subset-Family of TRC such that
    A27: for x be set holds x in G0 iff x in bool carr & P[x] from SUBSET_1:sch
1;
   A28: for k be Nat st 1<=k & k<len E for x be Element of bool bool carr ex y
be Element of bool bool carr st P[k,x,y]
   proof
    let k be Nat such that
     1<=k and
     k<len E;
    let x be Element of bool bool carr;
    set y={g where g is Subset of TRC:g in G & (g c=f.(k+1) or g in x)};
    y c=bool carr
    proof
     let z be set;
     assume z in y;
     then ex g be Subset of TRC st g=z & g in G & (g c=f.(k+1) or g in x);
     hence thesis;
    end;
    hence thesis;
   end;
   consider p be FinSequence of bool bool carr such that
    A29: len p=len E and
    A30: p/.1=G0 or len E=0 and
    A31: for k be Nat st 1<=k & k<len E holds P[k,p/.k,p/.(k+1)] from NAT_2:sch
1(A28);
   defpred H[Nat,set] means
    ($1=1 implies $2=union G0) & ($1<>1 implies $2=union(p.$1\p.($1-1)));
   A32: for k be Nat st k in Seg len E ex x be set st H[k,x]
   proof
    let k be Nat;
    k=1 or k<>1;
    hence thesis;
   end;
   consider h be FinSequence such that
    A33: dom h=Seg len E and
    A34: for k be Nat st k in Seg len E holds H[k,h.k] from FINSEQ_1:sch 1(A32
);
   A35: dom p=Seg len E by A29,FINSEQ_1:def 3;
   rng h c=bool carr
   proof
    let y be set;
    assume y in rng h;
    then consider x be set such that
     A36: x in dom h and
     A37: h.x=y by FUNCT_1:def 3;
    reconsider x as Nat by A36;
    p.x in rng p by A35,A33,A36,FUNCT_1:def 3;
    then reconsider px=p.x as Subset-Family of TRC;
    y=union G0 or y=union(px\p.(x-1)) by A33,A34,A36,A37;
    hence thesis;
   end;
   then reconsider h as FinSequence of bool carr by FINSEQ_1:def 4;
   A38: A is non empty affinely-independent Subset of TOP-REAL n by A1;
   A39: 1<=n+1 by NAT_1:11;
   the carrier of TRC c=union rng h
   proof
    let x be set;
    assume x in the carrier of TRC;
    then x in union G by A24,SETFAM_1:45;
    then consider y be set such that
     A40: x in y and
     A41: y in G by TARSKI:def 4;
    consider z be set such that
     A42: z in R and
     A43: y c=z by A25,A41,SETFAM_1:def 2;
    consider k be set such that
     A44: k in dom f and
     A45: f.k=z by A42,FUNCT_1:def 3;
    reconsider k as Nat by A44;
    A46: k>=1 by A44,FINSEQ_3:25;
    A47: len E>=k by A5,A44,FINSEQ_3:25;
    per cases by A46,XXREAL_0:1;
    suppose A48: k=1 or y in G0;
     A49: 1 in Seg len E by A1,A10,A39,FINSEQ_1:1;
     then A50: h.1=union G0 by A34;
     y in G0 by A27,A41,A43,A45,A48;
     then A51: x in h.1 by A40,A50,TARSKI:def 4;
     h.1 in rng h by A33,A49,FUNCT_1:def 3;
     hence thesis by A51,TARSKI:def 4;
    end;
    suppose A52: k>1 & not y in G0;
     defpred Q[Nat] means
      $1>1 & $1<=len E & y c=f.$1;
     A53: ex k be Nat st Q[k] by A43,A45,A47,A52;
     consider m be Nat such that
      A54: Q[m] & for n be Nat st Q[n] holds m<=n from NAT_1:sch 5(A53);
     reconsider m1=m-1 as Element of NAT by A54,NAT_1:20;
     defpred R[Nat] means
      1<=$1 & $1<=m1 implies not y in p/.$1;
     m1+1<=len E by A54;
     then A55: m1<len E by NAT_1:13;
     A56: for n be Nat st R[n] holds R[n+1]
     proof
      let n be Nat such that
       A57: R[n];
      set n1=n+1;
      assume that
       1<=n1 and
       A58: n1<=m1;
      n<m1 by A58,NAT_1:13;
      then A59: n<len E by A55,XXREAL_0:2;
      per cases by NAT_1:14;
      suppose n=0;
       hence thesis by A1,A9,A30,A52,FINSEQ_4:62;
      end;
      suppose A60: n>=1;
       assume A61: y in p/.n1;
       p/.n1={g where g is Subset of TRC:g in G & (g c=f.n1 or g in p/.n)} by
A31,A59,A60;
       then ex g be Subset of TRC st y=g & g in G & (g c=f.n1 or g in p/.n) by
A61;
       then Q[n1] by A55,A57,A58,A60,NAT_1:13,XXREAL_0:2;
       then m<=n1 by A54;
       then m1+1<=m1 by A58,XXREAL_0:2;
       hence contradiction by NAT_1:13;
      end;
     end;
     A62: R[0];
     A63: for n holds R[n] from NAT_1:sch 2(A62,A56);
     A64: m in dom p by A29,A54,FINSEQ_3:25;
     then A65: h.m in rng h by A35,A33,FUNCT_1:def 3;
     m1+1>1 by A54;
     then A66: m1>=1 by NAT_1:13;
     then A67: p/.m={g where g is Subset of TRC:g in G & (g c=f.(m1+1) or g in
p/.m1)} by A31,A55;
     m1 in dom p by A29,A66,A55,FINSEQ_3:25;
     then p.m1=p/.m1 by PARTFUN1:def 6;
     then A68: not y in p.m1 by A66,A63;
     p.m=p/.m by A64,PARTFUN1:def 6;
     then y in p.m by A41,A54,A67;
     then y in p.m\p.m1 by A68,XBOOLE_0:def 5;
     then A69: x in union(p.m\p.m1) by A40,TARSKI:def 4;
     h.m=union(p.m\p.m1) by A35,A34,A54,A64;
     hence thesis by A69,A65,TARSKI:def 4;
    end;
   end;
   then A70: rng h is Cover of TRC by SETFAM_1:def 11;
   now let A be Subset of TRC;
    assume A in rng h;
    then consider k be set such that
     A71: k in dom h and
     A72: h.k=A by FUNCT_1:def 3;
    reconsider k as Nat by A71;
    A73: k>=1 by A33,A71,FINSEQ_1:1;
    per cases by A73,XXREAL_0:1;
    suppose A74: k=1;
     A75: G0 c=G
     proof
      let x be set;
      assume x in G0;
      hence thesis by A27;
     end;
     h.k=union G0 by A33,A34,A71,A74;
     hence A is open by A23,A72,A75,TOPS_2:11,19;
    end;
    suppose A76: k>1;
     then reconsider k1=k-1 as Element of NAT by NAT_1:20;
     k1+1>1 by A76;
     then A77: k1>=1 by NAT_1:13;
     k1+1<=len E by A33,A71,FINSEQ_1:1;
     then A78: k1<len E by NAT_1:13;
     then k1 in dom p by A29,A77,FINSEQ_3:25;
     then A79: p.k1=p/.k1 by PARTFUN1:def 6;
     A80: P[k1,p/.k1,p/.(k1+1)] by A31,A77,A78;
     p/.k c=G
     proof
      let x be set;
      assume x in p/.k;
      then ex g be Subset of TRC st x=g & g in G & (g c=f.k or g in p/.k1) by
A80;
      hence thesis;
     end;
     then p/.k is open by A23,TOPS_2:11;
     then A81: p/.k\p/.(k-1) is open by TOPS_2:15;
     A82: p.k=p/.k by A35,A33,A71,PARTFUN1:def 6;
     A=union(p.k\p.(k-1)) by A33,A34,A71,A72,A76;
     hence A is open by A82,A81,A79,TOPS_2:19;
    end;
   end;
   then A83: rng h is open by TOPS_2:def 1;
   TRC is compact by COMPTS_1:3;
   then consider gx be Subset-Family of TRC such that
    gx is open and
    A84: gx is Cover of TRC and
    A85: clf gx is_finer_than rng h and
    A86: gx is locally_finite by A4,A70,A83,PCOMPS_1:22,PCOMPS_2:3;
   set cgx=clf gx;
   defpred G[set,set] means
    $2=union{u where u is Subset of TRC:u in cgx & u c=h.$1};
   A87: for k be Nat st k in Seg len E ex x be Element of bool carr st G[k,x]
   proof
    let k be Nat;
    set U={u where u is Subset of TRC:u in cgx & u c=h.k};
    U c=bool carr
    proof
     let x be set;
     assume x in U;
     then ex u be Subset of TRC st u=x & u in cgx & u c=h.k;
     hence thesis;
    end;
    then reconsider U as Subset-Family of TRC;
    union U is Subset of TRC;
    hence thesis;
   end;
   consider GX be FinSequence of bool carr such that
    A88: dom GX=Seg len E & for k be Nat st k in Seg len E holds G[k,GX.k]
from FINSEQ_1:sch 5(A87);
   A89: for i be Nat st i in dom GX holds GX.i c=h.i
   proof
    let i be Nat;
    set U={u where u is Subset of TRC:u in cgx & u c=h.i};
    now let x be set;
     assume x in U;
     then ex u be Subset of TRC st x=u & u in cgx & u c=h.i;
     hence x c=h.i;
    end;
    then A90: union U c=h.i by ZFMISC_1:76;
    assume i in dom GX;
    hence thesis by A88,A90;
   end;
   A91: dom E=Seg len E by FINSEQ_1:def 3;
   A92: for k be Nat st k in Seg len E holds h.k misses conv(A\{E.k})
   proof
    let k be Nat;
    assume A93: k in Seg len E;
    then A94: k>=1 by FINSEQ_1:1;
    A95: H[k,h.k] by A34,A93;
    assume h.k meets conv(A\{E.k});
    then consider x be set such that
     A96: x in h.k and
     A97: x in conv(A\{E.k}) by XBOOLE_0:3;
    per cases by A94,XXREAL_0:1;
    suppose A98: k=1;
     then consider y be set such that
      A99: x in y and
      A100: y in G0 by A95,A96,TARSKI:def 4;
     P[y] by A27,A100;
     then y c=F(k) by A5,A11,A91,A93,A98;
     hence contradiction by A97,A99,XBOOLE_0:def 5;
    end;
    suppose A101: k>1;
     then reconsider k1=k-1 as Element of NAT by NAT_1:20;
     len E>=k1+1 by A93,FINSEQ_1:1;
     then A102: len E>k1 by NAT_1:13;
     k1+1>1 by A101;
     then A103: k1>=1 by NAT_1:13;
     then A104: P[k1,p/.k1,p/.(k1+1)] by A31,A102;
     k1 in dom p by A29,A103,A102,FINSEQ_3:25;
     then A105: p/.k1=p.k1 by PARTFUN1:def 6;
     A106: p/.k=p.k by A35,A93,PARTFUN1:def 6;
     consider y be set such that
      A107: x in y and
      A108: y in p.k\p.(k-1) by A95,A96,A101,TARSKI:def 4;
     y in p.k by A108;
     then consider g be Subset of TRC such that
      A109: y=g and
      g in G and
      A110: g c=f.k or g in p.k1 by A104,A106,A105;
     f.k=F(k) by A5,A11,A91,A93;
     hence contradiction by A97,A107,A108,A109,A110,XBOOLE_0:def 5;
    end;
   end;
   carr c=union rng GX
   proof
    let x be set;
    assume A111: x in carr;
    union gx=carr & union gx c=union cgx by A84,PCOMPS_1:19,SETFAM_1:45;
    then consider y be set such that
     A112: x in y and
     A113: y in cgx by A111,TARSKI:def 4;
    consider r be set such that
     A114: r in rng h and
     A115: y c=r by A85,A113,SETFAM_1:def 2;
    consider k be set such that
     A116: k in dom h and
     A117: h.k=r by A114,FUNCT_1:def 3;
    A118: G[k,GX.k] by A33,A88,A116;
    A119: GX.k in rng GX by A33,A88,A116,FUNCT_1:def 3;
    y in {u where u is Subset of TRC:u in cgx & u c=h.k} by A113,A115,A117;
    then x in GX.k by A112,A118,TARSKI:def 4;
    hence thesis by A119,TARSKI:def 4;
   end;
   then A120: rng GX is Cover of TRC by SETFAM_1:def 11;
   A121: for S be Subset of dom GX holds conv(E.:S)c=union(GX.:S)
   proof
    let S be Subset of dom GX;
    A122: rng GX=GX.:dom GX by RELAT_1:113;
    A123: union rng GX=carr by A120,SETFAM_1:45;
    per cases by XBOOLE_0:def 10;
    suppose S=dom GX;
     hence thesis by A6,A9,A91,A88,A122,A123,RELAT_1:113;
    end;
    suppose A124: not dom GX c=S;
     set U={conv(A\{E.i}) where i is Element of NAT:i in dom E\S};
     dom GX\S is non empty by A124,XBOOLE_1:37;
     then A125: conv(E.:S)=meet U by A91,A88,Th12;
     A126: meet U misses union(GX.:(dom E\S))
     proof
      assume meet U meets union(GX.:(dom E\S));
      then consider x be set such that
       A127: x in meet U and
       A128: x in union(GX.:(dom E\S)) by XBOOLE_0:3;
      consider y be set such that
       A129: x in y and
       A130: y in GX.:(dom E\S) by A128,TARSKI:def 4;
      consider i be set such that
       A131: i in dom GX and
       A132: i in dom E\S and
       A133: GX.i=y by A130,FUNCT_1:def 6;
      reconsider i as Element of NAT by A131;
      conv(A\{E.i}) in U by A132;
      then A134: meet U c=conv(A\{E.i}) by SETFAM_1:7;
      y c=h.i by A89,A131,A133;
      then h.i meets conv(A\{E.i}) by A127,A129,A134,XBOOLE_0:3;
      hence contradiction by A92,A88,A131;
     end;
     dom GX=dom E by A88,FINSEQ_1:def 3;
     then rng GX=GX.:(S\/(dom E\S)) by A122,XBOOLE_1:45
      .=GX.:S\/GX.:(dom E\S) by RELAT_1:120;
     then A135: union(GX.:S)\/union(GX.:(dom E\S)) =C by A6,A123,ZFMISC_1:78;
     conv(E.:S)c=C by A9,RELAT_1:111,RLAFFIN1:3;
     hence thesis by A125,A135,A126,XBOOLE_1:73;
    end;
   end;
   A136: cgx is locally_finite by A86,PCOMPS_1:18;
   now let A be Subset of TRC;
    assume A in rng GX;
    then consider k be set such that
     A137: k in dom GX & GX.k=A by FUNCT_1:def 3;
    set U={u where u is Subset of TRC:u in cgx & u c=h.k};
    A138: U c=cgx
    proof
     let x be set;
     assume x in U;
     then ex u be Subset of TRC st x=u & u in cgx & u c=h.k;
     hence thesis;
    end;
    then reconsider U as Subset-Family of TRC by XBOOLE_1:1;
    U is closed by A138,PCOMPS_1:11,TOPS_2:12;
    then union U is closed by A136,A138,PCOMPS_1:9,21;
    hence A is closed by A88,A137;
   end;
   then A139: rng GX is closed by TOPS_2:def 2;
   len GX=card A by A10,A88,FINSEQ_1:def 3;
   then meet rng GX is non empty by A139,A38,A121,Th22;
   then consider I be set such that
    A140: I in meet rng GX by XBOOLE_0:def 1;
   defpred T[Nat,set] means
    $2 in G & I in $2 & $2 in p.$1 & ($1<>1 implies not$2 in p.($1-1));
   A141: for k be Nat st k in Seg len E ex x be Element of bool carr st T[k,x]
   proof
    let k be Nat;
    assume A142: k in Seg len E;
    then A143: k>=1 by FINSEQ_1:1;
    A144: k<=len E by A142,FINSEQ_1:1;
    A145: GX.k c=h.k & H[k,h.k] by A34,A88,A89,A142;
    GX.k in rng GX by A88,A142,FUNCT_1:def 3;
    then meet rng GX c=GX.k by SETFAM_1:7;
    then A146: I in GX.k by A140;
    per cases by A143,XXREAL_0:1;
    suppose A147: k=1;
     1 in dom p by A1,A10,A35,A39,FINSEQ_1:1;
     then A148: p.1=G0 by A1,A9,A30,FINSEQ_4:62,PARTFUN1:def 6;
     consider g be set such that
      A149: I in g and
      A150: g in G0 by A146,A145,A147,TARSKI:def 4;
     g in G by A27,A150;
     hence thesis by A147,A149,A150,A148;
    end;
    suppose A151: k>1;
     then reconsider k1=k-1 as Nat by NAT_1:20;
     A152: k1+1=k;
     then A153: k1<len E by A144,NAT_1:13;
     k1>=1 by A151,A152,NAT_1:13;
     then A154: P[k1,p/.k1,p/.k] by A31,A153;
     A155: p.k=p/.k by A35,A142,PARTFUN1:def 6;
     consider g be set such that
      A156: I in g and
      A157: g in p.k\p.(k-1) by A146,A145,A151,TARSKI:def 4;
     A158: not g in p.(k-1) by A157,XBOOLE_0:def 5;
     g in p.k by A157;
     then ex gg be Subset of TRC st g=gg & gg in G & (gg c=f.(k1+1) or gg in p
/.k1) by A154,A155;
     hence thesis by A156,A157,A158;
    end;
   end;
   consider t be FinSequence of bool carr such that
    A159: dom t=Seg len E & for k be Nat st k in Seg len E holds T[k,t.k] from
FINSEQ_1:sch 5(A141);
   A160: now let i,j be Nat;
    assume that
     A161: i in dom t and
     A162: j in dom t and
     A163: i<j;
    A164: j<=len E by A159,A162,FINSEQ_1:1;
    defpred P[Nat] means
     i<=$1 & $1<j implies t.i in p.$1;
    A165: T[i,t.i] by A159,A161;
    A166: 1<=i by A159,A161,FINSEQ_1:1;
    A167: for k st P[k] holds P[k+1]
    proof
     let k;
     assume A168: P[k];
     set k1=k+1;
     assume that
      A169: i<=k1 and
      A170: k1<j;
     A171: k<j by A170,NAT_1:13;
     per cases by A169,NAT_1:8;
     suppose i=k1;
      hence thesis by A159,A161;
     end;
     suppose A172: i<=k;
      1<=k1 & k1<=len E by A166,A164,A169,A170,XXREAL_0:2;
      then A173: k1 in dom p by A35,FINSEQ_1:1;
      A174: k<len E by A164,A171,XXREAL_0:2;
      A175: 1<=k by A166,A172,XXREAL_0:2;
      then k in dom p by A35,A174,FINSEQ_1:1;
      then A176: p.k=p/.k by PARTFUN1:def 6;
      P[k,p/.k,p/.k1] by A31,A175,A174;
      then p.k1={g where g is Subset of TRC:g in G & (g c=f.k1 or g in p.k)}
by A173,A176,PARTFUN1:def 6;
      hence thesis by A165,A168,A170,A172,NAT_1:13;
     end;
    end;
    A177: P[0] by A165;
    A178: for k holds P[k] from NAT_1:sch 2(A177,A167);
    reconsider j1=j-1 as Nat by A163,NAT_1:20;
    assume A179: t.i=t.j;
    A180: j1+1=j;
    then A181: j1<j by NAT_1:13;
    A182: j<>1 by A159,A161,A163,FINSEQ_1:1;
    i<=j1 by A163,A180,NAT_1:13;
    then t.i in p.j1 by A181,A178;
    hence contradiction by A159,A162,A179,A182;
   end;
   now let x1,x2 be set;
    assume A183: x1 in dom t & x2 in dom t;
    then reconsider i1=x1,i2=x2 as Nat;
    assume A184: t.x1=t.x2;
    assume x1<>x2;
    then i1>i2 or i1<i2 by XXREAL_0:1;
    hence contradiction by A160,A183,A184;
   end;
   then t is one-to-one by FUNCT_1:def 4;
   then A185: card rng t=len t by FINSEQ_4:62
    .=len E by A159,FINSEQ_1:def 3
    .=n+1 by A1,A9,FINSEQ_4:62;
   then A186: rng t is non empty;
   A187: now let x be set;
    assume x in rng t;
    then consider i be set such that
     A188: i in dom t & t.i=x by FUNCT_1:def 3;
    thus I in x by A159,A188;
   end;
   A189: rng t c=G
   proof
    let y be set;
    assume y in rng t;
    then consider x be set such that
     A190: x in dom t & t.x=y by FUNCT_1:def 3;
    thus thesis by A159,A190;
   end;
   n<card rng t by A185,NAT_1:13;
   then card n in card card rng t by NAT_1:41;
   then n1+1 in card rng t by CARD_1:42;
   then meet rng t is empty by A26,A189,TOPDIM_2:2;
   hence contradiction by A186,A187,SETFAM_1:def 1;
  end;
  ind C<=ind TR & ind TR<=n by TOPDIM_1:20,TOPDIM_2:21;
  then ind C<=n by XXREAL_0:2;
  hence thesis by A2,XXREAL_0:1;
 end;

theorem
  ind TOP-REAL n = n
  proof
   set T=TOP-REAL n;
   consider I be affinely-independent Subset of T such that
   A1:  {}T c= I & I c= [#]T & Affin I = Affin [#]T by RLAFFIN1:60;
   [#]T is Affine by RUSUB_4:22;
   then dim T = n & Affin [#]T = [#]T by RLAFFIN1:50,RLAFFIN3:4;
   then card I = n+1 by A1,RLAFFIN3:6;
   then ind conv I=n by Th25;
   then ind T >= n & ind T <= n by TOPDIM_1:20,TOPDIM_2:21;
   hence thesis by XXREAL_0:1;
 end;