:: Chains on a Grating in Euclidean Space
::  by Freek Wiedijk
::
:: Received January 27, 2003
:: Copyright (c) 2003-2012 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NUMBERS, SUBSET_1, XREAL_0, ORDINAL1, ARYTM_3, REAL_1, XXREAL_0,
      CARD_1, XBOOLE_0, TARSKI, ZFMISC_1, SETFAM_1, XCMPLX_0, FINSEQ_1,
      FINSET_1, ABIAN, FUNCT_1, FINSEQ_2, FUNCT_2, RELAT_1, CARD_3, GOBOARD5,
      MCART_1, ARYTM_1, TREES_2, POLYNOM1, WAYBEL25, GRAPH_1, NAT_1, ORDERS_2,
      STRUCT_0, VECTSP_1, SUPINF_2, BINOP_1, ALGSTR_0, RLVECT_1, GROUP_6,
      CHAIN_1, MSSUBFAM;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, RELAT_1, ORDINAL1,
      XCMPLX_0, XXREAL_0, XREAL_0, FUNCT_1, REAL_1, EUCLID, FUNCT_2, ABIAN,
      CARD_1, DOMAIN_1, MOD_4, CARD_3, BINOP_1, SEQ_1, VECTSP_1, NAT_1,
      NUMBERS, FINSET_1, STRUCT_0, ALGSTR_0, FINSEQ_1, FINSEQ_2,
      RLVECT_1;
 constructors REAL_1, CARD_3, REALSET1, ABIAN, EUCLID, SEQ_1, RELSET_1,
      MOD_4;
 registrations XBOOLE_0, SUBSET_1, FINSET_1, NUMBERS, XXREAL_0, XREAL_0, NAT_1,
      MEMBERED, FINSEQ_1, ABIAN, STRUCT_0, VECTSP_1, CARD_1, VALUED_0,
      ZFMISC_1, RELAT_1, EUCLID, CARD_2, RELSET_1;
 requirements NUMERALS, SUBSET, BOOLE, REAL, ARITHM;
 definitions TARSKI, FUNCT_1, RLVECT_1, SUBSET_1, BINOP_1, STRUCT_0, ALGSTR_0,
      ZFMISC_1, FINSET_1;
 theorems TARSKI, ZFMISC_1, FINSEQ_1, SUBSET_1, XBOOLE_0, CARD_1, FINSEQ_2,
      FUNCT_2, EUCLID, NAT_1, XBOOLE_1, CARD_2, MCART_1, FUNCT_1, DOMAIN_1,
      ENUMSET1, CARD_3, XREAL_0, XREAL_1, XXREAL_0, ORDINAL1, VECTSP_1,
      XTUPLE_0;
 schemes CLASSES1, FRAENKEL, FUNCT_2, FINSET_1, LMOD_7, BINOP_1;

begin :: stuff I could not find in MML

reserve X,x,y,z for set;
reserve n,m,k,k9,d9 for Element of NAT;

theorem Th1:
  for x,y being real number st x < y ex z being Real st x < z & z < y
proof
  let x,y be real number;
  assume x < y;
  then consider z being real number such that
A1: x < z and
A2: z < y by XREAL_1:5;
  reconsider z as Real by XREAL_0:def 1;
  take z;
  thus thesis by A1,A2;
end;

theorem Th2:
  for x,y being real number ex z being Real st x < z & y < z
proof
  let x,y be real number;
  reconsider x,y as Real by XREAL_0:def 1;
  take z = max(x,y) + 1;
A1: x + 0 < z by XREAL_1:8,XXREAL_0:25;
  y + 0 < z by XREAL_1:8,XXREAL_0:25;
  hence thesis by A1;
end;

scheme FrSet12 { D()->non empty set, A()->non empty set, P[set,set],
  F(set,set)->Element of D() } :
  { F(x,y) where x,y is Element of A() : P[x,y] } c= D()
proof
  let z;
  assume z in { F(x,y) where x,y is Element of A() : P[x,y] };
  then ex x,y being Element of A() st z = F(x,y) & P[x,y];
  hence thesis;
end;

:: Subset A -> Subset B

definition
  let B be set;
  let A be Subset of B;
  redefine func bool A -> Subset-Family of B;
  coherence by ZFMISC_1:67;
end;

:: non-zero numbers

definition
  let d be real Element of NAT;
  redefine attr d is zero means
  not d > 0;
  compatibility;
end;

definition
  let d be Element of NAT;
  redefine attr d is zero means
  :Def2:
  not d >= 1;
  compatibility
  proof
    d is non zero iff d >= 1 + 0 by NAT_1:13;
    hence thesis;
  end;
end;

reserve d for non zero Element of NAT;
reserve i,i0,i1 for Element of Seg d;

:: non trivial sets

theorem Th3:
  {x,y} is trivial iff x = y
proof
  hereby
A1: x in {x,y} by TARSKI:def 2;
    y in {x,y} by TARSKI:def 2;
    hence {x,y} is trivial implies x = y by A1,ZFMISC_1:def 10;
  end;
  {x,x} = {x} by ENUMSET1:29;
  hence thesis;
end;

registration
  cluster non trivial finite for set;
  existence
  proof
    take {0,1};
    thus thesis by Th3;
  end;
end;

registration
  let X be non trivial set;
  let Y be set;
  cluster X \/ Y -> non trivial;
  coherence
  proof
    consider x,y such that
A1: x in X and
A2: y in X and
A3: x <> y by ZFMISC_1:def 10;
    take x,y;
    thus thesis by A1,A2,A3,XBOOLE_0:def 3;
  end;
  cluster Y \/ X -> non trivial;
  coherence;
end;

registration
  let X be non trivial set;
  cluster non trivial finite for Subset of X;
  existence
  proof
    consider x,y such that
A1: x in X and
A2: y in X and
A3: x <> y by ZFMISC_1:def 10;
    take {x,y};
    thus thesis by A1,A2,A3,Th3,ZFMISC_1:32;
  end;
end;

theorem Th4:
  X is trivial & X \/ {y} is non trivial implies ex x st X = {x}
proof
  assume that
A1: X is trivial and
A2: X \/ {y} is non trivial;
  X is empty or ex x st X = {x} by A1,ZFMISC_1:131;
  hence thesis by A2;
end;

scheme NonEmptyFinite
  { X()->non empty set, A()->non empty finite Subset of X(), P[set] } : P[A()]
provided
A1: for x being Element of X() st x in A() holds P[{x}] and
A2: for x being Element of X(), B being non empty finite Subset of X()
st x in A() & B c= A() & not x in B & P[B] holds P[B \/ {x}]
proof
  defpred Q[set] means $1 is empty or P[$1];
A3: A() is finite;
A4: Q[{}];
A5: for x,B being set st x in A() & B c= A() & Q[B] holds Q[B \/ {x}]
  proof
    let x,B be set;
    assume that
A6: x in A() and
A7: B c= A() and
A8: Q[B];
    reconsider B as Subset of X() by A7,XBOOLE_1:1;
    per cases;
    suppose x in B;
      then {x} c= B by ZFMISC_1:31;
      hence thesis by A8,XBOOLE_1:12;
    end;
    suppose
      B is non empty & not x in B;
      hence thesis by A2,A6,A7,A8;
    end;
    suppose B is empty;
      hence thesis by A1,A6;
    end;
  end;
  Q[A()] from FINSET_1:sch 2(A3,A4,A5);
  hence thesis;
end;

scheme NonTrivialFinite
  { X()->non trivial set, A()->non trivial finite Subset of X(), P[set] } :
  P[A()]
provided
A1: for x,y being Element of X() st x in A() & y in A() & x <> y
holds P[{x,y}] and
A2: for x being Element of X(), B being non trivial finite Subset of X()
st x in A() & B c= A() & not x in B & P[B] holds P[B \/ {x}]
proof
  defpred Q[set] means $1 is trivial or P[$1];
A3: A() is finite;
A4: Q[{}];
A5: for x,B being set st x in A() & B c= A() & Q[B] holds Q[B \/ {x}]
  proof
    let x,B be set;
    assume that
A6: x in A() and
A7: B c= A() and
A8: Q[B];
    reconsider B as Subset of X() by A7,XBOOLE_1:1;
    per cases;
    suppose B \/ {x} is trivial;
      hence thesis;
    end;
    suppose x in B;
      then {x} c= B by ZFMISC_1:31;
      hence thesis by A8,XBOOLE_1:12;
    end;
    suppose
      B is non trivial & not x in B;
      hence thesis by A2,A6,A7,A8;
    end;
    suppose
A9:   B is trivial & B \/ {x} is non trivial;
      then consider y being set such that
A10:  B = {y} by Th4;
A11:  x <> y by A9,A10;
A12:  B \/ {x} = {x,y} by A10,ENUMSET1:1;
      y in B by A10,TARSKI:def 1;
      hence thesis by A1,A6,A7,A11,A12;
    end;
  end;
  Q[A()] from FINSET_1:sch 2(A3,A4,A5);
  hence thesis;
end;

:: sets of cardinality 2

theorem Th5:
  card X = 2 iff
  ex x,y st x in X & y in X & x <> y & for z st z in X holds z = x or z = y
proof
  hereby
    assume
A1: card X = 2;
    then reconsider X9 = X as finite set;
    consider x,y such that
A2: x <> y and
A3: X9 = {x,y} by A1,CARD_2:60;
    take x,y;
    thus x in X & y in X & x <> y &
    for z st z in X holds z = x or z = y by A2,A3,TARSKI:def 2;
  end;
  given x,y such that
A4: x in X and
A5: y in X and
A6: x <> y and
A7: for z st z in X holds z = x or z = y;
  for z holds z in X iff z = x or z = y by A4,A5,A7;
  then X = {x,y} by TARSKI:def 2;
  hence thesis by A6,CARD_2:57;
end;

theorem
  (m is even iff n is even) iff m + n is even;

theorem Th7:
  for X,Y being finite set st X misses Y holds
  (card X is even iff card Y is even) iff card(X \/ Y) is even
proof
  let X,Y be finite set;
  assume X misses Y;
  then card(X \/ Y) = card X + card Y by CARD_2:40;
  hence thesis;
end;

theorem Th8:
  for X,Y being finite set holds
  (card X is even iff card Y is even) iff card(X \+\ Y) is even
proof
  let X,Y be finite set;
A1: X \ Y misses X /\ Y by XBOOLE_1:89;
A2: X = (X \ Y) \/ (X /\ Y) by XBOOLE_1:51;
A3: Y \ X misses X /\ Y by XBOOLE_1:89;
A4: Y = (Y \ X) \/ (X /\ Y) by XBOOLE_1:51;
A5: X \ Y misses Y \ X by XBOOLE_1:82;
A6: X \+\ Y = (X \ Y) \/ (Y \ X) by XBOOLE_0:def 6;
A7: (card(X \ Y) is even iff card(X /\ Y) is even) iff card X is even by A1,A2
,Th7;
  (card(Y \ X) is even iff card(X /\ Y) is even) iff card Y is even by A3,A4
,Th7;
  hence thesis by A5,A6,A7,Th7;
end;

:: elements of REAL d as functions to REAL

definition
  let n;
  redefine func REAL n means
  :Def3:
  for x holds x in it iff x is Function of Seg n,REAL;
  compatibility
  proof
A1: for x holds x in REAL n iff x is Function of Seg n,REAL
    proof
      let x;
      hereby
        assume x in REAL n;
        then x in n-tuples_on REAL by EUCLID:def 1;
        then x in Funcs(Seg n,REAL) by FINSEQ_2:93;
        hence x is Function of Seg n,REAL by FUNCT_2:66;
      end;
      assume x is Function of Seg n,REAL;
      then x in Funcs(Seg n,REAL) by FUNCT_2:8;
      then x in n-tuples_on REAL by FINSEQ_2:93;
      hence thesis by EUCLID:def 1;
    end;
    let X be FinSequenceSet of REAL;
    thus
    X = REAL n implies for x holds x in X iff x is Function of Seg n,REAL
    by A1;
    assume
A2: for x holds x in X iff x is Function of Seg n,REAL;
    now
      let x;
      x in X iff x is Function of Seg n,REAL by A2;
      hence x in X iff x in REAL n by A1;
    end;
    hence thesis by TARSKI:1;
  end;
end;

reserve l,r,l9,r9,l99,r99,x,x9,l1,r1,l2,r2 for Element of REAL d;
reserve Gi for non trivial finite Subset of REAL;
reserve li,ri,li9,ri9,xi,xi9 for Real;

begin :: gratings, cells, chains, cycles
:: gratings

definition
  let d;
  mode Grating of d -> Function of Seg d,bool REAL means
    :Def4:
    for i holds it.i is non trivial finite;
  existence
  proof
    defpred P[set,set] means $2 is non trivial finite Subset of REAL;
A1: for i being set st i in Seg d ex X being set st P[i,X]
    proof
      let i being set;
      assume i in Seg d;
      set X = the non trivial finite Subset of REAL;
      take X;
      thus thesis;
    end;
    consider G being Function such that
A2: dom G = Seg d &
    for i being set st i in Seg d holds P[i,G.i] from CLASSES1:sch 1(A1);
    for i being set st i in Seg d holds G.i in bool REAL
    proof
      let i be set;
      assume i in Seg d;
      then G.i is Subset of REAL by A2;
      hence thesis;
    end;
    then reconsider G as Function of Seg d,bool REAL by A2,FUNCT_2:3;
    take G;
    thus thesis by A2;
  end;
end;

reserve G for Grating of d;

registration
  let d;
 cluster -> finite-yielding for Grating of d;
 coherence
  proof let G;
   let i be set;
   assume i in Seg d;
   hence G.i is finite by Def4;
  end;
end;

definition
  let d,G,i;
  redefine func G.i -> non trivial finite Subset of REAL;
  coherence by Def4;
end;

theorem Th9:
  x in product G iff for i holds x.i in G.i
proof
  x is Function of Seg d,REAL by Def3;
  then
A1: dom x = Seg d by FUNCT_2:def 1;
A2: dom G = Seg d by FUNCT_2:def 1;
  hence x in product G implies for i holds x.i in G.i by CARD_3:9;
  assume for i holds x.i in G.i;
  then for i being set st i in Seg d holds x.i in G.i;
  hence thesis by A1,A2,CARD_3:9;
end;

:: gaps

canceled;

theorem Th11:
  for X being non empty finite Subset of REAL holds
  ex ri st ri in X & for xi st xi in X holds ri >= xi
proof
  defpred P[set] means ex ri st ri in $1 & for xi st xi in $1 holds ri >= xi;
  let X be non empty finite Subset of REAL;
A1: for xi st xi in X holds P[{xi}]
  proof
    let xi;
    assume xi in X;
    take xi;
    thus thesis by TARSKI:def 1;
  end;
A2: for x being Real, B being non empty finite Subset of REAL st
  x in X & B c= X & not x in B & P[B] holds P[B \/ {x}]
  proof
    let x be Real;
    let B be non empty finite Subset of REAL;
    assume that x in X and B c= X
    and not x in B and
A3: P[B];
    consider ri such that
A4: ri in B and
A5: for xi st xi in B holds ri >= xi by A3;
    set B9 = B \/ {x};
A6: now
      let xi;
      xi in {x} iff xi = x by TARSKI:def 1;
      hence xi in B9 iff xi in B or xi = x by XBOOLE_0:def 3;
    end;
    per cases;
    suppose
A7:   x <= ri;
      take ri;
      thus ri in B9 by A4,A6;
      let xi;
      assume xi in B9;
      then xi in B or xi = x by A6;
      hence thesis by A5,A7;
    end;
    suppose
A8:   ri < x;
      take x;
      thus x in B9 by A6;
      let xi;
      assume xi in B9;
      then xi in B or xi = x by A6;
      then ri >= xi or xi = x by A5;
      hence thesis by A8,XXREAL_0:2;
    end;
  end;
  thus P[X] from NonEmptyFinite(A1,A2);
end;

theorem Th12:
  for X being non empty finite Subset of REAL holds
  ex li st li in X & for xi st xi in X holds li <= xi
proof
  defpred P[set] means ex li st li in $1 & for xi st xi in $1 holds li <= xi;
  let X be non empty finite Subset of REAL;
A1: for xi st xi in X holds P[{xi}]
  proof
    let xi;
    assume xi in X;
    take xi;
    thus thesis by TARSKI:def 1;
  end;
A2: for x being Real, B being non empty finite Subset of REAL st
  x in X & B c= X & not x in B & P[B] holds P[B \/ {x}]
  proof
    let x be Real;
    let B be non empty finite Subset of REAL;
    assume that x in X and B c= X
    and not x in B and
A3: P[B];
    consider li such that
A4: li in B and
A5: for xi st xi in B holds li <= xi by A3;
    set B9 = B \/ {x};
A6: now
      let xi;
      xi in {x} iff xi = x by TARSKI:def 1;
      hence xi in B9 iff xi in B or xi = x by XBOOLE_0:def 3;
    end;
    per cases;
    suppose
A7:   li <= x;
      take li;
      thus li in B9 by A4,A6;
      let xi;
      assume xi in B9;
      then xi in B or xi = x by A6;
      hence thesis by A5,A7;
    end;
    suppose
A8:   x < li;
      take x;
      thus x in B9 by A6;
      let xi;
      assume xi in B9;
      then xi in B or xi = x by A6;
      then li <= xi or xi = x by A5;
      hence thesis by A8,XXREAL_0:2;
    end;
  end;
  thus P[X] from NonEmptyFinite(A1,A2);
end;

theorem Th13:
  ex li,ri st li in Gi & ri in Gi &
  li < ri & for xi st xi in Gi holds not (li < xi & xi < ri)
proof
  defpred P[set] means ex li,ri st li in $1 & ri in $1 &
  li < ri & for xi st xi in $1 holds not (li < xi & xi < ri);
A1: now
    let li,ri;
    assume that
    li in Gi and ri in Gi and
A2: li <> ri;
A3: now
      let li,ri;
      assume
A4:   li < ri;
      thus P[{li,ri}]
      proof
        take li,ri;
        thus thesis by A4,TARSKI:def 2;
      end;
    end;
    li < ri or ri < li by A2,XXREAL_0:1;
    hence P[{li,ri}] by A3;
  end;
A5: for x being Real, B being non trivial finite Subset of REAL
  st x in Gi & B c= Gi & not x in B & P[B] holds P[B \/ {x}]
  proof
    let x be Real;
    let B be non trivial finite Subset of REAL;
    assume that
    x in Gi and B c= Gi and
A6: not x in B and
A7: P[B];
    consider li,ri such that
A8: li in B and
A9: ri in B and
A10: li < ri and
A11: for xi st xi in B holds not (li < xi & xi < ri) by A7;
    per cases by A6,A8,A9,XXREAL_0:1;
    suppose
A12:  x < li;
      take li,ri;
      thus li in B \/ {x} & ri in B \/ {x} & li < ri by A8,A9,A10,
XBOOLE_0:def 3;
      let xi;
      assume xi in B \/ {x};
      then xi in B or xi in {x} by XBOOLE_0:def 3;
      hence thesis by A11,A12,TARSKI:def 1;
    end;
    suppose
A13:  li < x & x < ri;
      take li,x;
      x in {x} by TARSKI:def 1;
      hence li in B \/ {x} & x in B \/ {x} & li < x by A8,A13,XBOOLE_0:def 3;
      let xi;
      assume xi in B \/ {x};
      then xi in B or xi in {x} by XBOOLE_0:def 3;
      then not (li < xi & xi < ri) or xi = x by A11,TARSKI:def 1;
      hence thesis by A13,XXREAL_0:2;
    end;
    suppose
A14:  ri < x;
      take li,ri;
      thus li in B \/ {x} & ri in B \/ {x} & li < ri by A8,A9,A10,
XBOOLE_0:def 3;
      let xi;
      assume xi in B \/ {x};
      then xi in B or xi in {x} by XBOOLE_0:def 3;
      hence thesis by A11,A14,TARSKI:def 1;
    end;
  end;
  thus P[Gi] from NonTrivialFinite(A1,A5);
end;

theorem
  for X being non empty finite Subset of REAL holds
  ex ri st ri in X & for xi st xi in X holds ri >= xi by Th11;

theorem
  ex li,ri st li in Gi & ri in Gi &
  ri < li & for xi st xi in Gi holds not (xi < ri or li < xi)
proof
  consider li such that
A1: li in Gi and
A2: for xi st xi in Gi holds li >= xi by Th11;
  consider ri such that
A3: ri in Gi and
A4: for xi st xi in Gi holds ri <= xi by Th12;
  take li,ri;
A5: ri <= li by A2,A3;
  now
    assume
A6: li = ri;
    consider x1,x2 be set such that
A7: x1 in Gi and
A8: x2 in Gi and
A9: x1 <> x2 by ZFMISC_1:def 10;
    reconsider x1,x2 as Real by A7,A8;
A10: ri <= x1 by A4,A7;
A11: x1 <= li by A2,A7;
A12: ri <= x2 by A4,A8;
A13: x2 <= li by A2,A8;
    x1 = li by A6,A10,A11,XXREAL_0:1;
    hence contradiction by A6,A9,A12,A13,XXREAL_0:1;
  end;
  hence thesis by A1,A2,A3,A4,A5,XXREAL_0:1;
end;

definition
  let Gi;
  mode Gap of Gi -> Element of [:REAL,REAL:] means
    :Def5:
    ex li,ri st it = [li,ri] & li in Gi & ri in Gi &
    ((li < ri & for xi st xi in Gi holds not (li < xi & xi < ri)) or
    (ri < li & for xi st xi in Gi holds not (li < xi or xi < ri)));
  existence
  proof
    consider li,ri such that
A1: li in Gi and
A2: ri in Gi and
A3: li < ri and
A4: for xi st xi in Gi holds not (li < xi & xi < ri) by Th13;
    take [li,ri],li,ri;
    thus thesis by A1,A2,A3,A4;
  end;
end;

theorem Th16:
  [li,ri] is Gap of Gi iff li in Gi & ri in Gi &
  ((li < ri & for xi st xi in Gi holds not (li < xi & xi < ri)) or
  (ri < li & for xi st xi in Gi holds not (li < xi or xi < ri)))
proof
  thus [li,ri] is Gap of Gi implies li in Gi & ri in Gi &
  ((li < ri & for xi st xi in Gi holds not (li < xi & xi < ri)) or
  (ri < li & for xi st xi in Gi holds not (li < xi or xi < ri)))
  proof
    assume [li,ri] is Gap of Gi;
    then consider li9,ri9 such that
A1: [li,ri] = [li9,ri9] and
A2: li9 in Gi and
A3: ri9 in Gi and
A4: (li9 < ri9 & for xi st xi in Gi holds not (li9 < xi & xi < ri9)) or
    (ri9 < li9 & for xi st xi in Gi holds not (li9 < xi or xi < ri9))
    by Def5;
A5: li9 = li by A1,XTUPLE_0:1;
    ri9 = ri by A1,XTUPLE_0:1;
    hence thesis by A2,A3,A4,A5;
  end;
  thus thesis by Def5;
end;

theorem
  Gi = {li,ri} implies
  ([li9,ri9] is Gap of Gi iff li9 = li & ri9 = ri or li9 = ri & ri9 = li)
proof
  assume
A1: Gi = {li,ri};
  hereby
    assume
A2: [li9,ri9] is Gap of Gi;
    then
A3: li9 in Gi by Th16;
A4: ri9 in Gi by A2,Th16;
A5: li9 = li or li9 = ri by A1,A3,TARSKI:def 2;
    li9 <> ri9 by A2,Th16;
    hence li9 = li & ri9 = ri or li9 = ri & ri9 = li by A1,A4,A5,TARSKI:def 2;
  end;
  for Gi,li,ri st Gi = {li,ri} holds [li,ri] is Gap of Gi
  proof
    let Gi,li,ri;
    assume
A6: Gi = {li,ri};
    take li,ri;
    thus [li,ri] = [li,ri] & li in Gi & ri in Gi by A6,TARSKI:def 2;
    li <> ri by A6,Th3;
    hence thesis by A6,TARSKI:def 2,XXREAL_0:1;
  end;
  hence thesis by A1;
end;

deffunc f(set) = $1;

theorem Th18:
  xi in Gi implies ex ri st [xi,ri] is Gap of Gi
proof
  assume
A1: xi in Gi;
  defpred P[Real] means $1 > xi;
  set Gi9 = { f(ri9) : f(ri9) in Gi & P[ri9]};
A2: Gi9 c= Gi from FRAENKEL:sch 17;
  then reconsider Gi9 as finite Subset of REAL by XBOOLE_1:1;
  per cases;
  suppose
A3: Gi9 is empty;
A4: now
      let xi9;
      assume that
A5:   xi9 in Gi and
A6:   xi9 > xi;
      xi9 in Gi9 by A5,A6;
      hence contradiction by A3;
    end;
    consider li such that
A7: li in Gi and
A8: for xi9 st xi9 in Gi holds li <= xi9 by Th12;
    take li;
A9: now
      assume
A10:  li = xi;
      for xi9 being set holds xi9 in Gi iff xi9 = xi
      proof
        let xi9 be set;
        hereby
          assume
A11:      xi9 in Gi;
          then reconsider xi99 = xi9 as Element of REAL;
A12:      li <= xi99 by A8,A11;
          xi99 <= xi by A4,A11;
          hence xi9 = xi by A10,A12,XXREAL_0:1;
        end;
        thus thesis by A1;
      end;
      hence Gi = {xi} by TARSKI:def 1;
      hence contradiction;
    end;
    li <= xi by A1,A8;
    then
A13: li < xi by A9,XXREAL_0:1;
    for xi9 st xi9 in Gi holds not (xi < xi9 or xi9 < li) by A4,A8;
    hence thesis by A1,A7,A13,Th16;
  end;
  suppose Gi9 is non empty;
    then reconsider Gi9 as non empty finite Subset of REAL;
    consider ri such that
A14: ri in Gi9 and
A15: for ri9 st ri9 in Gi9 holds ri9 >= ri by Th12;
    take ri;
    now
      thus xi in Gi by A1;
      thus ri in Gi by A2,A14;
      ex ri9 st ri9 = ri & ri9 in Gi & xi < ri9 by A14;
      hence xi < ri;
      hereby
        let xi9;
        assume xi9 in Gi;
        then xi9 <= xi or xi9 in Gi9;
        hence not (xi < xi9 & xi9 < ri) by A15;
      end;
    end;
    hence thesis by Th16;
  end;
end;

theorem Th19:
  xi in Gi implies ex li st [li,xi] is Gap of Gi
proof
  assume
A1: xi in Gi;
  defpred P[Real] means $1 < xi;
  set Gi9 = { f(li9) : f(li9) in Gi & P[li9]};
A2: Gi9 c= Gi from FRAENKEL:sch 17;
  then reconsider Gi9 as finite Subset of REAL by XBOOLE_1:1;
  per cases;
  suppose
A3: Gi9 is empty;
A4: now
      let xi9;
      assume that
A5:   xi9 in Gi and
A6:   xi9 < xi;
      xi9 in Gi9 by A5,A6;
      hence contradiction by A3;
    end;
    consider ri such that
A7: ri in Gi and
A8: for xi9 st xi9 in Gi holds ri >= xi9 by Th11;
    take ri;
A9: now
      assume
A10:  ri = xi;
      for xi9 being set holds xi9 in Gi iff xi9 = xi
      proof
        let xi9 be set;
        hereby
          assume
A11:      xi9 in Gi;
          then reconsider xi99 = xi9 as Element of REAL;
A12:      ri >= xi99 by A8,A11;
          xi99 >= xi by A4,A11;
          hence xi9 = xi by A10,A12,XXREAL_0:1;
        end;
        thus thesis by A1;
      end;
      hence Gi = {xi} by TARSKI:def 1;
      hence contradiction;
    end;
    ri >= xi by A1,A8;
    then
A13: ri > xi by A9,XXREAL_0:1;
    for xi9 st xi9 in Gi holds not (xi9 > ri or xi > xi9) by A4,A8;
    hence thesis by A1,A7,A13,Th16;
  end;
  suppose Gi9 is non empty;
    then reconsider Gi9 as non empty finite Subset of REAL;
    consider li such that
A14: li in Gi9 and
A15: for li9 st li9 in Gi9 holds li9 <= li by Th11;
    take li;
    now
      thus xi in Gi by A1;
      thus li in Gi by A2,A14;
      ex li9 st li9 = li & li9 in Gi & xi > li9 by A14;
      hence xi > li;
      hereby
        let xi9;
        assume xi9 in Gi;
        then xi9 >= xi or xi9 in Gi9;
        hence not (xi9 > li & xi > xi9) by A15;
      end;
    end;
    hence thesis by Th16;
  end;
end;

theorem Th20:
  [li,ri] is Gap of Gi & [li,ri9] is Gap of Gi implies ri = ri9
proof
A1: ri <= ri9 & ri9 <= ri implies ri = ri9 by XXREAL_0:1;
  assume that
A2: [li,ri] is Gap of Gi and
A3: [li,ri9] is Gap of Gi;
A4: ri in Gi by A2,Th16;
A5: ri9 in Gi by A3,Th16;
  per cases by A2,Th16;
  suppose
A6: li < ri & for xi st xi in Gi holds not (li < xi & xi < ri);
    ri9 <= li or li < ri9 & ri9 < ri or ri <= ri9;
    hence thesis by A1,A3,A4,A5,A6,Th16;
  end;
  suppose
A7: ri < li & for xi st xi in Gi holds not (li < xi or xi < ri);
    ri9 < ri or ri <= ri9 & ri9 <= li or li < ri9;
    hence thesis by A1,A3,A4,A5,A7,Th16;
  end;
end;

theorem Th21:
  [li,ri] is Gap of Gi & [li9,ri] is Gap of Gi implies li = li9
proof
A1: li <= li9 & li9 <= li implies li = li9 by XXREAL_0:1;
  assume that
A2: [li,ri] is Gap of Gi and
A3: [li9,ri] is Gap of Gi;
A4: li in Gi by A2,Th16;
A5: li9 in Gi by A3,Th16;
  per cases by A2,Th16;
  suppose
A6: li < ri & for xi st xi in Gi holds not (li < xi & xi < ri);
    li9 <= li or li < li9 & li9 < ri or ri <= li9;
    hence thesis by A1,A3,A4,A5,A6,Th16;
  end;
  suppose
A7: ri < li & for xi st xi in Gi holds not (li < xi or xi < ri);
    li9 < ri or ri <= li9 & li9 <= li or li < li9;
    hence thesis by A1,A3,A4,A5,A7,Th16;
  end;
end;

theorem Th22:
  ri < li & [li,ri] is Gap of Gi & ri9 < li9 & [li9,ri9] is Gap of Gi implies
  li = li9 & ri = ri9
proof
  assume that
A1: ri < li and
A2: [li,ri] is Gap of Gi and
A3: ri9 < li9 and
A4: [li9,ri9] is Gap of Gi;
A5: li in Gi by A2,Th16;
A6: ri in Gi by A2,Th16;
A7: li9 in Gi by A4,Th16;
A8: ri9 in Gi by A4,Th16;
  hereby
    assume li <> li9;
    then li < li9 or li9 < li by XXREAL_0:1;
    hence contradiction by A1,A2,A3,A4,A5,A7,Th16;
  end;
  hereby
    assume ri <> ri9;
    then ri < ri9 or ri9 < ri by XXREAL_0:1;
    hence contradiction by A1,A2,A3,A4,A6,A8,Th16;
  end;
end;

:: cells, chains

definition
  let d,l,r;
  func cell(l,r) -> non empty Subset of REAL d equals
  { x : (for i holds l.i <= x.i & x.i <= r.i) or
  (ex i st r.i < l.i & (x.i <= r.i or l.i <= x.i)) };
  coherence
  proof
    defpred P[Element of REAL d] means
    (for i holds l.i <= $1.i & $1.i <= r.i) or
    (ex i st r.i < l.i & ($1.i <= r.i or l.i <= $1.i));
    set CELL = { x : P[x] };
    P[l];
    then
A1: l in CELL;
    CELL c= REAL d from FRAENKEL:sch 10;
    hence thesis by A1;
  end;
end;

theorem Th23:
  x in cell(l,r) iff ((for i holds l.i <= x.i & x.i <= r.i) or
  ex i st r.i < l.i & (x.i <= r.i or l.i <= x.i) )
proof
  defpred P[Element of REAL d] means (for i holds l.i <= $1.i & $1.i <= r.i) or
  (ex i st r.i < l.i & ($1.i <= r.i or l.i <= $1.i));
A1: cell(l,r) = { x9 :  P[x9] };
  thus x in cell(l,r) iff P[x] from LMOD_7:sch 7(A1);
end;

theorem Th24:
  (for i holds l.i <= r.i) implies
  (x in cell(l,r) iff for i holds l.i <= x.i & x.i <= r.i)
proof
  assume
A1: for i holds l.i <= r.i;
  hereby
    assume x in cell(l,r);
    then (for i holds l.i <= x.i & x.i <= r.i) or
    ex i st r.i < l.i & (x.i <= r.i or l.i <= x.i) by Th23;
    hence for i holds l.i <= x.i & x.i <= r.i by A1;
  end;
  thus thesis;
end;

theorem Th25:
  (ex i st r.i < l.i) implies
  (x in cell(l,r) iff ex i st r.i < l.i & (x.i <= r.i or l.i <= x.i))
proof
  given i0 such that
A1: r.i0 < l.i0;
  x.i0 < l.i0 or r.i0 < x.i0 by A1,XXREAL_0:2;
  hence
  x in cell(l,r) implies ex i st r.i < l.i & (x.i <= r.i or l.i <= x.i)
  by Th23;
  thus thesis;
end;

theorem Th26:
  l in cell(l,r) & r in cell(l,r)
proof
A1: (for i holds l.i <= l.i & l.i <= r.i) or ex i st r.i < l.i & (l.i <= r
  .i or l.i <= l.i);
  (for i holds l.i <= r.i & r.i <= r.i) or ex i st r.i < l.i & (r.i <= r
  .i or l.i <= r.i);
  hence thesis by A1;
end;

theorem Th27:
  cell(x,x) = {x}
proof
  for x9 being set holds x9 in cell(x,x) iff x9 = x
  proof
    let x9 be set;
    thus x9 in cell(x,x) implies x9 = x
    proof
      assume
A1:   x9 in cell(x,x);
      then reconsider x,x9 as Function of Seg d,REAL by Def3;
      now
        let i;
A2:     for i holds x.i <= x.i;
        then
A3:     x.i <= x9.i by A1,Th24;
        x9.i <= x.i by A1,A2,Th24;
        hence x9.i = x.i by A3,XXREAL_0:1;
      end;
      hence thesis by FUNCT_2:63;
    end;
    thus thesis by Th26;
  end;
  hence thesis by TARSKI:def 1;
end;

theorem Th28:
  (for i holds l9.i <= r9.i) implies (cell(l,r) c= cell(l9,r9) iff
  for i holds l9.i <= l.i & l.i <= r.i & r.i <= r9.i)
proof
  assume
A1: for i holds l9.i <= r9.i;
  thus cell(l,r) c= cell(l9,r9) implies
  for i holds l9.i <= l.i & l.i <= r.i & r.i <= r9.i
  proof
    assume
A2: cell(l,r) c= cell(l9,r9);
    let i0;
    per cases;
    suppose
A3:   r.i0 < l.i0;
      defpred P[Element of Seg d,Real] means $2 > l.$1 & $2 > r9.$1;
A4:   for i ex xi st P[i,xi] by Th2;
      consider x being Function of Seg d,REAL such that
A5:   for i holds P[i,x.i] from FUNCT_2:sch 3(A4);
      reconsider x as Element of REAL d by Def3;
      ex i st r.i < l.i & (x.i <= r.i or l.i <= x.i)
      proof
        take i0;
        thus thesis by A3,A5;
      end;
      then
A6:   x in cell(l,r);
      ex i st x.i < l9.i or r9.i < x.i
      proof
        take i0;
        thus thesis by A5;
      end;
      hence thesis by A1,A2,A6,Th24;
    end;
    suppose
A7:   l.i0 <= r.i0;
A8:   l in cell(l,r) by Th26;
      r in cell(l,r) by Th26;
      hence thesis by A1,A2,A7,A8,Th24;
    end;
  end;
  assume
A9: for i holds l9.i <= l.i & l.i <= r.i & r.i <= r9.i;
  let x be set;
  assume
A10: x in cell(l,r);
  then reconsider x as Element of REAL d;
  now
    let i;
A11: l9.i <= l.i by A9;
A12: l.i <= x.i by A9,A10,Th24;
A13: x.i <= r.i by A9,A10,Th24;
    r.i <= r9.i by A9;
    hence l9.i <= x.i & x.i <= r9.i by A11,A12,A13,XXREAL_0:2;
    hence l9.i <= r9.i by XXREAL_0:2;
  end;
  hence thesis;
end;

theorem Th29:
  (for i holds r.i < l.i) implies (cell(l,r) c= cell(l9,r9) iff
  for i holds r.i <= r9.i & r9.i < l9.i & l9.i <= l.i)
proof
  assume
A1: for i holds r.i < l.i;
  thus cell(l,r) c= cell(l9,r9) implies
  for i holds r.i <= r9.i & r9.i < l9.i & l9.i <= l.i
  proof
    assume
A2: cell(l,r) c= cell(l9,r9);
A3: for i holds r9.i < l9.i
    proof
      let i0;
      assume
A4:   l9.i0 <= r9.i0;
      defpred P[Element of Seg d,Real] means
      ($1 = i0 implies l.$1 < $2 & r9.$1 < $2) &
      (r9.$1 < l9.$1 implies r9.$1 < $2 & $2 < l9.$1);
A5:   for i ex xi st P[i,xi]
      proof
        let i;
        per cases;
        suppose i = i0 & r9.i < l9.i;
          hence thesis by A4;
        end;
        suppose
A6:       i <> i0;
          r9.i < l9.i implies ex xi st r9.i < xi & xi < l9.i by Th1;
          hence thesis by A6;
        end;
        suppose
A7:       l9.i <= r9.i;
          ex xi st l.i < xi & r9.i < xi by Th2;
          hence thesis by A7;
        end;
      end;
      consider x being Function of Seg d,REAL such that
A8:   for i holds P[i,x.i] from FUNCT_2:sch 3(A5);
      reconsider x as Element of REAL d by Def3;
A9:   r.i0 < l.i0 by A1;
      x.i0 <= r.i0 or l.i0 <= x.i0 by A8;
      then
A10:  x in cell(l,r) by A9;
      per cases by A2,A10,Th23;
      suppose for i holds l9.i <= x.i & x.i <= r9.i;
        then x.i0 <= r9.i0;
        hence contradiction by A8;
      end;
      suppose ex i st r9.i < l9.i & (x.i <= r9.i or l9.i <= x.i);
        hence contradiction by A8;
      end;
    end;
    let i0;
    hereby
      assume
A11:  r9.i0 < r.i0;
      defpred P[Element of Seg d,Real] means
      r9.$1 < $2 & $2 < l9.$1 & ($1 = i0 implies $2 < r.$1);
A12:  for i ex xi st P[i,xi]
      proof
        let i;
        per cases;
        suppose
A13:      i = i0 & l9.i <= r.i;
          r9.i < l9.i by A3;
          then consider xi such that
A14:      r9.i < xi and
A15:      xi < l9.i by Th1;
          xi < r.i by A13,A15,XXREAL_0:2;
          hence thesis by A14,A15;
        end;
        suppose
A16:      i = i0 & r.i <= l9.i;
          then consider xi such that
A17:      r9.i < xi and
A18:      xi < r.i by A11,Th1;
          xi < l9.i by A16,A18,XXREAL_0:2;
          hence thesis by A17,A18;
        end;
        suppose
A19:      i <> i0;
          r9.i < l9.i by A3;
          then ex xi st ( r9.i < xi)&( xi < l9.i) by Th1;
          hence thesis by A19;
        end;
      end;
      consider x being Function of Seg d,REAL such that
A20:  for i holds P[i,x.i] from FUNCT_2:sch 3(A12);
      reconsider x as Element of REAL d by Def3;
A21:  r.i0 < l.i0 by A1;
      x.i0 <= r.i0 or l.i0 <= x.i0 by A20;
      then
A22:  x in cell(l,r) by A21;
      not (l9.i0 <= x.i0 & x.i0 <= r9.i0) by A3,XXREAL_0:2;
      then ex i st r9.i < l9.i & (x.i <= r9.i or l9.i <= x.i) by A2,A22,Th23;
      hence contradiction by A20;
    end;
    thus r9.i0 < l9.i0 by A3;
    hereby
      assume
A23:  l9.i0 > l.i0;
      defpred R[Element of Seg d,Real] means
      l9.$1 > $2 & $2 > r9.$1 & ($1 = i0 implies $2 > l.$1);
A24:  for i ex xi st R[i,xi]
      proof
        let i;
        per cases;
        suppose
A25:      i = i0 & r9.i >= l.i;
          l9.i > r9.i by A3;
          then consider xi such that
A26:      r9.i < xi and
A27:      xi < l9.i by Th1;
          xi > l.i by A25,A26,XXREAL_0:2;
          hence thesis by A26,A27;
        end;
        suppose
A28:      i = i0 & l.i >= r9.i;
          then consider xi such that
A29:      l.i < xi and
A30:      xi < l9.i by A23,Th1;
          xi > r9.i by A28,A29,XXREAL_0:2;
          hence thesis by A29,A30;
        end;
        suppose
A31:      i <> i0;
          l9.i > r9.i by A3;
          then ex xi st ( r9.i < xi)&( xi < l9.i) by Th1;
          hence thesis by A31;
        end;
      end;
      consider x being Function of Seg d,REAL such that
A32:  for i holds R[i,x.i] from FUNCT_2:sch 3(A24);
      reconsider x as Element of REAL d by Def3;
A33:  l.i0 > r.i0 by A1;
      x.i0 >= l.i0 or r.i0 >= x.i0 by A32;
      then
A34:  x in cell(l,r) by A33;
      not (r9.i0 >= x.i0 & x.i0 >= l9.i0) by A3,XXREAL_0:2;
      then ex i st l9.i > r9.i & (x.i <= r9.i or l9.i <= x.i) by A2,A34,Th23;
      hence contradiction by A32;
    end;
  end;
  assume
A35: for i holds r.i <= r9.i & r9.i < l9.i & l9.i <= l.i;
  let x be set;
  assume
A36: x in cell(l,r);
  then reconsider x as Element of REAL d;
  set i0 = the Element of Seg d;
A37: r.i0 <= r9.i0 by A35;
  r9.i0 < l9.i0 by A35;
  then
A38: r.i0 < l9.i0 by A37,XXREAL_0:2;
  l9.i0 <= l.i0 by A35;
  then r.i0 < l.i0 by A38,XXREAL_0:2;
  then x.i0 < l.i0 or r.i0 < x.i0 by XXREAL_0:2;
  then consider i such that
  r.i < l.i and
A39: x.i <= r.i or l.i <= x.i by A36,Th23;
A40: r.i <= r9.i by A35;
A41: l9.i <= l.i by A35;
A42: r9.i < l9.i by A35;
  x.i <= r9.i or l9.i <= x.i by A39,A40,A41,XXREAL_0:2;
  hence thesis by A42;
end;

theorem Th30:
  (for i holds l.i <= r.i) & (for i holds r9.i < l9.i) implies
  (cell(l,r) c= cell(l9,r9) iff ex i st r.i <= r9.i or l9.i <= l.i)
proof
  assume
A1: for i holds l.i <= r.i;
  assume
A2: for i holds r9.i < l9.i;
  thus
  cell(l,r) c= cell(l9,r9) implies ex i st r.i <= r9.i or l9.i <= l.i
  proof
    assume
A3: cell(l,r) c= cell(l9,r9);
    assume
A4: for i holds r9.i < r.i & l.i < l9.i;
    defpred P[Element of Seg d,Real] means
    l.$1 <= $2 & $2 <= r.$1 & r9.$1 < $2 & $2 < l9.$1;
A5: for i ex xi st P[i,xi]
    proof
      let i;
      per cases;
      suppose
A6:     l.i <= r9.i & l9.i <= r.i;
        r9.i < l9.i by A2;
        then consider xi such that
A7:     r9.i < xi and
A8:     xi < l9.i by Th1;
        take xi;
        thus thesis by A6,A7,A8,XXREAL_0:2;
      end;
      suppose
A9:     r9.i < l.i & l9.i <= r.i;
        take l.i;
        thus thesis by A1,A4,A9;
      end;
      suppose
A10:    r.i < l9.i;
        take r.i;
        thus thesis by A1,A4,A10;
      end;
    end;
    consider x being Function of Seg d,REAL such that
A11: for i holds P[i,x.i] from FUNCT_2:sch 3(A5);
    reconsider x as Element of REAL d by Def3;
A12: x in cell(l,r) by A11;
    set i0 = the Element of Seg d;
    r9.i0 < l9.i0 by A2;
    then ex i st r9.i < l9.i & (x.i <= r9.i or l9.i <= x.i) by A3,A12,Th25;
    hence contradiction by A11;
  end;
  given i0 such that
A13: r.i0 <= r9.i0 or l9.i0 <= l.i0;
  let x be set;
  assume
A14: x in cell(l,r);
  then reconsider x as Element of REAL d;
A15: l.i0 <= x.i0 by A1,A14,Th24;
A16: x.i0 <= r.i0 by A1,A14,Th24;
  ex i st r9.i < l9.i & (x.i <= r9.i or l9.i <= x.i)
  proof
    take i0;
    thus thesis by A2,A13,A15,A16,XXREAL_0:2;
  end;
  hence thesis;
end;

theorem Th31:
  (for i holds l.i <= r.i) or (for i holds l.i > r.i) implies
  (cell(l,r) = cell(l9,r9) iff l = l9 & r = r9)
proof
  assume
A1: (for i holds l.i <= r.i) or for i holds l.i > r.i;
  thus cell(l,r) = cell(l9,r9) implies l = l9 & r = r9
  proof
    assume
A2: cell(l,r) = cell(l9,r9);
    per cases by A1;
    suppose
A3:   for i holds l.i <= r.i;
      then
A4:   for i holds l.i <= l9.i & l9.i <= r9.i & r9.i <= r.i by A2,Th28;
      reconsider l,r,l9,r9 as Function of Seg d,REAL by Def3;
A5:   now
        let i;
A6:     l.i <= l9.i by A2,A3,Th28;
        l9.i <= l.i by A2,A4,Th28;
        hence l.i = l9.i by A6,XXREAL_0:1;
      end;
      now
        let i;
A7:     r.i <= r9.i by A2,A4,Th28;
        r9.i <= r.i by A2,A3,Th28;
        hence r.i = r9.i by A7,XXREAL_0:1;
      end;
      hence thesis by A5,FUNCT_2:63;
    end;
    suppose
A8:   for i holds l.i > r.i;
      then
A9:   for i holds r.i <= r9.i & r9.i < l9.i & l9.i <= l.i by A2,Th29;
      reconsider l,r,l9,r9 as Function of Seg d,REAL by Def3;
A10:  now
        let i;
A11:    l.i <= l9.i by A2,A9,Th29;
        l9.i <= l.i by A2,A8,Th29;
        hence l.i = l9.i by A11,XXREAL_0:1;
      end;
      now
        let i;
A12:    r.i <= r9.i by A2,A8,Th29;
        r9.i <= r.i by A2,A9,Th29;
        hence r.i = r9.i by A12,XXREAL_0:1;
      end;
      hence thesis by A10,FUNCT_2:63;
    end;
  end;
  thus thesis;
end;

definition
  let d,G,k;
  assume
A1: k <= d;
  func cells(k,G) -> finite non empty Subset-Family of REAL d equals
  :Def7:
  { cell(l,r) : ((ex X being Subset of Seg d st card X = k &
  for i holds (i in X & l.i < r.i & [l.i,r.i] is Gap of G.i) or
  (not i in X & l.i = r.i & l.i in G.i)) or
  (k = d & for i holds r.i < l.i & [l.i,r.i] is Gap of G.i)) };
  coherence
  proof
    defpred R[Element of REAL d,Element of REAL d] means
    ((ex X being Subset of Seg d st card X = k &
    for i holds (i in X & $1.i < $2.i & [$1.i,$2.i] is Gap of G.i) or
    (not i in X & $1.i = $2.i & $1.i in G.i)) or
    (k = d & for i holds $2.i < $1.i & [$1.i,$2.i] is Gap of G.i));
    deffunc f(Element of REAL d,Element of REAL d) = cell($1,$2);
    set CELLS = { f(l,r) : R[l,r] };
    reconsider X = Seg k as Subset of Seg d by A1,FINSEQ_1:5;
    defpred P[Element of Seg d,Element of [:REAL,REAL:]] means
    ($1 in X & ex li,ri st $2 = [li,ri] & li < ri & $2 is Gap of G.$1) or
    (not $1 in X & ex li st $2 = [li,li] & li in G.$1);
A2: now
      let i;
      thus ex lri being Element of [:REAL,REAL:] st P[i,lri]
      proof
        per cases;
        suppose
A3:       i in X;
          consider li,ri such that
A4:       li in G.i and
A5:       ri in G.i and
A6:       li < ri and
A7:       for xi st xi in G.i holds not (li < xi & xi < ri) by Th13;
          take [li,ri];
          [li,ri] is Gap of G.i by A4,A5,A6,A7,Def5;
          hence thesis by A3,A6;
        end;
        suppose
A8:       not i in X;
          set li = the Element of G.i;
          reconsider li as Real;
          reconsider lri = [li,li] as Element of [:REAL,REAL:];
          take lri;
          thus thesis by A8;
        end;
      end;
    end;
    consider lr being Function of Seg d,[:REAL,REAL:] such that
A9: for i holds P[i,lr.i] from FUNCT_2:sch 3(A2);
    deffunc l(Element of Seg d) = (lr.$1)`1;
    consider l being Function of Seg d,REAL such that
A10: for i holds l.i = l(i) from FUNCT_2:sch 4;
    deffunc r(Element of Seg d) = (lr.$1)`2;
    consider r being Function of Seg d,REAL such that
A11: for i holds r.i = r(i) from FUNCT_2:sch 4;
    reconsider l,r as Element of REAL d by Def3;
A12: now
      let i;
A13:  l.i = (lr.i)`1 by A10;
      r.i = (lr.i)`2 by A11;
      hence lr.i = [l.i,r.i] by A13,MCART_1:21;
    end;
    now
      take A = cell(l,r);
      thus A = cell(l,r);
      now
        take X;
        thus card X = k by FINSEQ_1:57;
        take l,r;
        thus A = cell(l,r);
        let i;
        per cases;
        suppose
A14:      i in X;
          then consider li,ri such that
A15:      lr.i = [li,ri] and
A16:      li < ri and
A17:      lr.i is Gap of G.i by A9;
A18:      lr.i = [l.i,r.i] by A12;
          then li = l.i by A15,XTUPLE_0:1;
          hence i in X & l.i < r.i & [l.i,r.i] is Gap of G.i or
          not i in X & l.i = r.i & l.i in G.i by A14,A15,A16,A17,A18,XTUPLE_0:1
;
        end;
        suppose
A19:      not i in X;
          then consider li such that
A20:      lr.i = [li,li] and
A21:      li in G.i by A9;
A22:      [li,li] = [l.i,r.i] by A12,A20;
          then li = l.i by XTUPLE_0:1;
          hence i in X & l.i < r.i & [l.i,r.i] is Gap of G.i or
          not i in X & l.i = r.i & l.i in G.i by A19,A21,A22,XTUPLE_0:1;
        end;
      end;
      hence ex l,r st A = cell(l,r) &
      ((ex X being Subset of Seg d st card X = k &
      for i holds (i in X & l.i < r.i & [l.i,r.i] is Gap of G.i) or
      (not i in X & l.i = r.i & l.i in G.i)) or
      (k = d & for i holds r.i < l.i & [l.i,r.i] is Gap of G.i));
    end;
    then
A23: cell(l,r) in CELLS;
    defpred Q[set,Element of REAL d,Element of REAL d,set] means
    $2 in product G & $3 in product G &
    (($4 = [0,[$2,$3]] & $1 = cell($2,$3)) or
    ($4 = [1,[$2,$3]] & $1 = cell($2,$3)));
    defpred S[set,set] means ex l,r st Q[$1,l,r,$2];
A24: for A being set st A in CELLS ex lr being set st S[A,lr]
    proof
      let A be set;
      assume A in CELLS;
      then consider l,r such that
A25:  A = cell(l,r) and
A26:  (ex X being Subset of Seg d st card X = k & for i holds (i in X &
l.i < r.i & [l.i,r.i] is Gap of G.i) or (not i in X & l.i = r.i & l.i in G.i))
      or (k = d & for i holds r.i < l.i & [l.i,r.i] is Gap of G.i);
      per cases by A26;
      suppose
A27:    ex X being Subset of Seg d st card X = k &
        for i holds i in X & l.i < r.i & [l.i,r.i] is Gap of G.i or
        not i in X & l.i = r.i & l.i in G.i;
        take [0,[l,r]],l,r;
        now
          let i;
          l.i < r.i & [l.i,r.i] is Gap of G.i or l.i = r.i & l.i in G.i by A27;
          hence l.i in G.i & r.i in G.i by Th16;
        end;
        hence l in product G & r in product G by Th9;
        thus thesis by A25;
      end;
      suppose
A28:    k = d & for i holds r.i < l.i & [l.i,r.i] is Gap of G.i;
        take [1,[l,r]],l,r;
        now
          let i;
          [l.i,r.i] is Gap of G.i by A28;
          hence l.i in G.i & r.i in G.i by Th16;
        end;
        hence l in product G & r in product G by Th9;
        thus thesis by A25;
      end;
    end;
    consider f being Function such that
A29: dom f = CELLS &
    for A being set st A in CELLS holds S[A,f.A] from CLASSES1:sch 1(A24);
A30: f is one-to-one
    proof
      let A,A9 be set;
      assume that
A31:  A in dom f and
A32:  A9 in dom f and
A33:  f.A = f.A9;
      consider l,r such that
A34:  Q[A,l,r,f.A] by A29,A31;
      consider l9,r9 such that
A35:  Q[A9,l9,r9,f.A9] by A29,A32;
      per cases by A34;
      suppose
A36:    f.A = [0,[l,r]] & A = cell(l,r);
        then
A37:    [l,r] = [l9,r9] by A33,A35,XTUPLE_0:1;
        then l = l9 by XTUPLE_0:1;
        hence thesis by A35,A36,A37,XTUPLE_0:1;
      end;
      suppose
A38:    f.A = [1,[l,r]] & A = cell(l,r);
        then
A39:    [l,r] = [l9,r9] by A33,A35,XTUPLE_0:1;
        then l = l9 by XTUPLE_0:1;
        hence thesis by A35,A38,A39,XTUPLE_0:1;
      end;
    end;
    reconsider X = product G as finite set;
A40: rng f c= [:{0,1},[:X,X:]:]
    proof
      let lr be set;
      assume lr in rng f;
      then consider A being set such that
A41:  A in dom f and
A42:  lr = f.A by FUNCT_1:def 3;
      consider l,r such that
A43:  Q[A,l,r,f.A] by A29,A41;
A44:  0 in {0,1} by TARSKI:def 2;
A45:  1 in {0,1} by TARSKI:def 2;
      [l,r] in [:X,X:] by A43,ZFMISC_1:87;
      hence thesis by A42,A43,A44,A45,ZFMISC_1:87;
    end;
    CELLS c= bool(REAL d) from FrSet12;
    hence thesis by A23,A29,A30,A40,CARD_1:59;
  end;
end;

theorem Th32:
  k <= d implies for A being Subset of REAL d holds A in cells(k,G) iff
  ex l,r st A = cell(l,r) & ((ex X being Subset of Seg d st card X = k &
  for i holds (i in X & l.i < r.i & [l.i,r.i] is Gap of G.i) or
  (not i in X & l.i = r.i & l.i in G.i)) or
  (k = d & for i holds r.i < l.i & [l.i,r.i] is Gap of G.i))
proof
  assume k <= d;
  then cells(k,G) = { cell(l,r) : ((ex X being Subset of Seg d st card X = k &
  for i holds (i in X & l.i < r.i & [l.i,r.i] is Gap of G.i) or
  (not i in X & l.i = r.i & l.i in G.i)) or
  (k = d & for i holds r.i < l.i & [l.i,r.i] is Gap of G.i)) } by Def7;
  hence thesis;
end;

theorem Th33:
  k <= d implies (cell(l,r) in cells(k,G) iff
  ((ex X being Subset of Seg d st card X = k &
  for i holds (i in X & l.i < r.i & [l.i,r.i] is Gap of G.i) or
  (not i in X & l.i = r.i & l.i in G.i)) or
  (k = d & for i holds r.i < l.i & [l.i,r.i] is Gap of G.i)))
proof
  assume
A1: k <= d;
  hereby
    assume cell(l,r) in cells(k,G);
    then consider l9,r9 such that
A2: cell(l,r) = cell(l9,r9) and
A3: (ex X being Subset of Seg d st card X = k & for i holds (i in X &
l9.i < r9.i & [l9.i,r9.i] is Gap of G.i) or (not i in X & l9.i = r9.i & l9.i in
    G.i)) or (k = d & for i holds r9.i < l9.i & [l9.i,r9.i] is Gap of G.i)
    by A1,Th32;
    l = l9 & r = r9
    proof
      per cases by A3;
      suppose ex X being Subset of Seg d st card X = k &
        for i holds i in X & l9.i < r9.i & [l9.i,r9.i] is Gap of G.i or
        not i in X & l9.i = r9.i & l9.i in G.i;
        then for i holds l9.i <= r9.i;
        hence thesis by A2,Th31;
      end;
      suppose for i holds r9.i < l9.i & [l9.i,r9.i] is Gap of G.i;
        hence thesis by A2,Th31;
      end;
    end;
    hence (ex X being Subset of Seg d st card X = k &
    for i holds (i in X & l.i < r.i & [l.i,r.i] is Gap of G.i) or
    (not i in X & l.i = r.i & l.i in G.i)) or
    (k = d & for i holds r.i < l.i & [l.i,r.i] is Gap of G.i) by A3;
  end;
  thus thesis by A1,Th32;
end;

theorem Th34:
  k <= d & cell(l,r) in cells(k,G) implies
  (for i holds (l.i < r.i & [l.i,r.i] is Gap of G.i) or
  (l.i = r.i & l.i in G.i)) or
  for i holds r.i < l.i & [l.i,r.i] is Gap of G.i
proof
  assume that
A1: k <= d and
A2: cell(l,r) in cells(k,G);
  per cases by A1,A2,Th33;
  suppose ex X being Subset of Seg d st card X = k &
    for i holds i in X & l.i < r.i & [l.i,r.i] is Gap of G.i or
    not i in X & l.i = r.i & l.i in G.i;
    hence thesis;
  end;
  suppose k = d & for i holds r.i < l.i & [l.i,r.i] is Gap of G.i;
    hence thesis;
  end;
end;

theorem Th35:
  k <= d & cell(l,r) in cells(k,G) implies for i holds l.i in G.i & r.i in G.i
proof
  assume that
A1: k <= d and
A2: cell(l,r) in cells(k,G);
  let i;
  l.i < r.i & [l.i,r.i] is Gap of G.i or l.i = r.i & l.i in G.i or
  r.i < l.i & [l.i,r.i] is Gap of G.i by A1,A2,Th34;
  hence thesis by Th16;
end;

theorem
  k <= d & cell(l,r) in cells(k,G) implies
  (for i holds l.i <= r.i) or for i holds r.i < l.i by Th34;

theorem Th37:
  for A being Subset of REAL d holds
  A in cells(0,G) iff ex x st A = cell(x,x) & for i holds x.i in G.i
proof
  let A be Subset of REAL d;
  hereby
    assume A in cells(0,G);
    then consider l,r such that
A1: A = cell(l,r) and
A2: (ex X being Subset of Seg d st card X = 0 & for i holds (i in X & l
.i < r.i & [l.i,r.i] is Gap of G.i) or (not i in X & l.i = r.i & l.i in G.i))
    or (0 = d & for i holds r.i < l.i & [l.i,r.i] is Gap of G.i)
    by Th32;
    consider X being Subset of Seg d such that
A3: card X = 0 and
A4: for i holds i in X & l.i < r.i & [l.i,r.i] is Gap of G.i or not i
    in X & l.i = r.i & l.i in G.i
    by A2;
    reconsider l9 = l, r9 = r as Function of Seg d,REAL by Def3;
    X = {} by A3;
    then
A5: for i holds l9.i = r9.i & l.i in G.i by A4;
    then l9 = r9 by FUNCT_2:63;
    hence ex x st A = cell(x,x) & for i holds x.i in G.i by A1,A5;
  end;
  given x such that
A6: A = cell(x,x) and
A7: for i holds x.i in G.i;
  ex X being Subset of Seg d st card X = 0 &
  for i holds i in X & x.i < x.i & [x.i,x.i] is Gap of G.i or
  not i in X & x.i = x.i & x.i in G.i
  proof
    reconsider X = {} as Subset of Seg d by XBOOLE_1:2;
    take X;
    thus thesis by A7;
  end;
  hence thesis by A6,Th32;
end;

theorem Th38:
  cell(l,r) in cells(0,G) iff l = r & for i holds l.i in G.i
proof
  hereby
    assume cell(l,r) in cells(0,G);
    then consider x such that
A1: cell(l,r) = cell(x,x) and
A2: for i holds x.i in G.i by Th37;
A3: for i holds x.i <= x.i;
    then l = x by A1,Th31;
    hence l = r & for i holds l.i in G.i by A1,A2,A3,Th31;
  end;
  thus thesis by Th37;
end;

theorem Th39:
  for A being Subset of REAL d holds A in cells(d,G) iff
  ex l,r st A = cell(l,r) & (for i holds [l.i,r.i] is Gap of G.i) &
  ((for i holds l.i < r.i) or for i holds r.i < l.i )
proof
  let A be Subset of REAL d;
  hereby
    assume A in cells(d,G);
    then consider l,r such that
A1: A = cell(l,r) and
A2: (ex X being Subset of Seg d st card X = d & for i holds (i in X & l
.i < r.i & [l.i,r.i] is Gap of G.i) or (not i in X & l.i = r.i & l.i in G.i))
    or (d = d & for i holds r.i < l.i & [l.i,r.i] is Gap of G.i)
    by Th32;
    thus
    ex l,r st A = cell(l,r) & (for i holds [l.i,r.i] is Gap of G.i) &
    ((for i holds l.i < r.i) or for i holds r.i < l.i )
    proof
      take l,r;
      per cases by A2;
      suppose ex X being Subset of Seg d st card X = d &
        for i holds i in X & l.i < r.i & [l.i,r.i] is Gap of G.i or
        not i in X & l.i = r.i & l.i in G.i;
        then consider X being Subset of Seg d such that
A3:     card X = d and
A4:     for i holds i in X & l.i < r.i & [l.i,r.i] is Gap of G.i or not i
        in X & l.i = r.i & l.i in G.i;
        card X = card Seg d by A3,FINSEQ_1:57;
        then not X c< Seg d by CARD_2:48;
        then X = Seg d by XBOOLE_0:def 8;
        hence thesis by A1,A4;
      end;
      suppose for i holds r.i < l.i & [l.i,r.i] is Gap of G.i;
        hence thesis by A1;
      end;
    end;
  end;
  given l,r such that
A5: A = cell(l,r) and
A6: for i holds [l.i,r.i] is Gap of G.i and
A7: (for i holds l.i < r.i) or for i holds r.i < l.i;
  per cases by A7;
  suppose
A8: for i holds l.i < r.i;
    ex X being Subset of Seg d st card X = d &
    for i holds i in X & l.i < r.i & [l.i,r.i] is Gap of G.i or
    not i in X & l.i = r.i & l.i in G.i
    proof
      Seg d c= Seg d;
      then reconsider X = Seg d as Subset of Seg d;
      take X;
      thus card X = d by FINSEQ_1:57;
      thus thesis by A6,A8;
    end;
    hence thesis by A5,Th32;
  end;
  suppose for i holds r.i < l.i;
    hence thesis by A5,A6,Th32;
  end;
end;

theorem Th40:
  cell(l,r) in cells(d,G) iff (for i holds [l.i,r.i] is Gap of G.i) &
  ((for i holds l.i < r.i) or for i holds r.i < l.i )
proof
  hereby
    assume cell(l,r) in cells(d,G);
    then consider l9,r9 such that
A1: cell(l,r) = cell(l9,r9) and
A2: for i holds [l9.i,r9.i] is Gap of G.i and
A3: (for i holds l9.i < r9.i) or for i holds r9.i < l9.i by Th39;
A4: (for i holds l9.i <= r9.i) or for i holds r9.i < l9.i by A3;
    then
A5: l = l9 by A1,Th31;
    r = r9 by A1,A4,Th31;
    hence (for i holds [l.i,r.i] is Gap of G.i) &
    ((for i holds l.i < r.i) or for i holds r.i < l.i ) by A2,A3,A5;
  end;
  thus thesis by Th39;
end;

theorem Th41:
  d = d9 + 1 implies for A being Subset of REAL d holds A in cells(d9,G) iff
  ex l,r,i0 st A = cell(l,r) & l.i0 = r.i0 & l.i0 in G.i0 &
  for i st i <> i0 holds l.i < r.i & [l.i,r.i] is Gap of G.i
proof
  assume
A1: d = d9 + 1;
  then
A2: d9 < d by NAT_1:13;
  let A be Subset of REAL d;
  hereby
    assume A in cells(d9,G);
    then consider l,r such that
A3: A = cell(l,r) and
A4: (ex X being Subset of Seg d st card X = d9 & for i holds (i in X &
l.i < r.i & [l.i,r.i] is Gap of G.i) or (not i in X & l.i = r.i & l.i in G.i))
    or (d9 = d & for i holds r.i < l.i & [l.i,r.i] is Gap of G.i)
    by A2,Th32;
    take l,r;
    consider X being Subset of Seg d such that
A5: card X = d9 and
A6: for i holds i in X & l.i < r.i & [l.i,r.i] is Gap of G.i or not i
    in X & l.i = r.i & l.i in G.i
    by A1,A4;
    card(Seg d \ X) = card Seg d - card X by CARD_2:44
      .= d - d9 by A5,FINSEQ_1:57
      .= 1 by A1;
    then consider i0 being set such that
A7: Seg d \ X = {i0} by CARD_2:42;
    i0 in Seg d \ X by A7,TARSKI:def 1;
    then reconsider i0 as Element of Seg d by XBOOLE_0:def 5;
    take i0;
A8: now
      let i;
      i in Seg d \ X iff i = i0 by A7,TARSKI:def 1;
      hence i in X iff i <> i0 by XBOOLE_0:def 5;
    end;
    thus A = cell(l,r) by A3;
    not i0 in X by A8;
    hence l.i0 = r.i0 & l.i0 in G.i0 by A6;
    let i;
    assume i <> i0;
    then i in X by A8;
    hence l.i < r.i & [l.i,r.i] is Gap of G.i by A6;
  end;
  given l,r,i0 such that
A9: A = cell(l,r) and
A10: l.i0 = r.i0 and
A11: l.i0 in G.i0 and
A12: for i st i <> i0 holds l.i < r.i & [l.i,r.i] is Gap of G.i;
  reconsider X = Seg d \ {i0} as Subset of Seg d by XBOOLE_1:36;
  card X = d9 & for i holds i in X & l.i < r.i & [l.i,r.i] is Gap of G.i or
  not i in X & l.i = r.i & l.i in G.i
  proof
    thus card X = card Seg d - card {i0} by CARD_2:44
      .= d - card {i0} by FINSEQ_1:57
      .= d - 1 by CARD_1:30
      .= d9 by A1;
    let i;
    i in {i0} iff i = i0 by TARSKI:def 1;
    hence thesis by A10,A11,A12,XBOOLE_0:def 5;
  end;
  hence thesis by A2,A9,Th32;
end;

theorem
  d = d9 + 1 implies (cell(l,r) in cells(d9,G) iff
  ex i0 st l.i0 = r.i0 & l.i0 in G.i0 &
  for i st i <> i0 holds l.i < r.i & [l.i,r.i] is Gap of G.i)
proof
  assume
A1: d = d9 + 1;
  hereby
    assume cell(l,r) in cells(d9,G);
    then consider l9,r9,i0 such that
A2: cell(l,r) = cell(l9,r9) and
A3: l9.i0 = r9.i0 and
A4: l9.i0 in G.i0 and
A5: for i st i <> i0 holds l9.i < r9.i & [l9.i,r9.i] is Gap of G.i by A1,Th41;
    take i0;
A6: now
      let i;
      i = i0 or i <> i0;
      hence l9.i <= r9.i by A3,A5;
    end;
    then
A7: l = l9 by A2,Th31;
    r = r9 by A2,A6,Th31;
    hence l.i0 = r.i0 & l.i0 in G.i0 &
    for i st i <> i0 holds l.i < r.i & [l.i,r.i] is Gap of G.i by A3,A4,A5,A7;
  end;
  thus thesis by A1,Th41;
end;

theorem Th43:
  for A being Subset of REAL d holds A in cells(1,G) iff
  ex l,r,i0 st A = cell(l,r) &
  (l.i0 < r.i0 or d = 1 & r.i0 < l.i0) & [l.i0,r.i0] is Gap of G.i0 &
  for i st i <> i0 holds l.i = r.i & l.i in G.i
proof
A1: d >= 1 by Def2;
  let A be Subset of REAL d;
  hereby
    assume A in cells(1,G);
    then consider l,r such that
A2: A = cell(l,r) and
A3: (ex X being Subset of Seg d st card X = 1 & for i holds (i in X & l
.i < r.i & [l.i,r.i] is Gap of G.i) or (not i in X & l.i = r.i & l.i in G.i))
    or (1 = d & for i holds r.i < l.i & [l.i,r.i] is Gap of G.i)
    by A1,Th32;
    take l,r;
    thus ex i0 st A = cell(l,r) &
    (l.i0 < r.i0 or d = 1 & r.i0 < l.i0) & [l.i0,r.i0] is Gap of G.i0 &
    for i st i <> i0 holds l.i = r.i & l.i in G.i
    proof
      per cases by A3;
      suppose ex X being Subset of Seg d st card X = 1 &
        for i holds i in X & l.i < r.i & [l.i,r.i] is Gap of G.i or
        not i in X & l.i = r.i & l.i in G.i;
        then consider X being Subset of Seg d such that
A4:     card X = 1 and
A5:     for i holds i in X & l.i < r.i & [l.i,r.i] is Gap of G.i or not i
        in X & l.i = r.i & l.i in G.i;
        consider i0 being set such that
A6:     X = {i0} by A4,CARD_2:42;
A7:     i0 in X by A6,TARSKI:def 1;
        then reconsider i0 as Element of Seg d;
        take i0;
        thus A = cell(l,r) &
        (l.i0 < r.i0 or d = 1 & r.i0 < l.i0) & [l.i0,r.i0] is Gap of G.i0
        by A2,A5,A7;
        let i;
        not i in X iff i <> i0 by A6,TARSKI:def 1;
        hence thesis by A5;
      end;
      suppose
A8:     d = 1 & for i holds r.i < l.i & [l.i,r.i] is Gap of G.i;
        reconsider i0 = 1 as Element of Seg d by A1,FINSEQ_1:1;
        take i0;
        thus A = cell(l,r) &
        (l.i0 < r.i0 or d = 1 & r.i0 < l.i0) & [l.i0,r.i0] is Gap of G.i0
        by A2,A8;
        let i;
A9:     1 <= i by FINSEQ_1:1;
        i <= d by FINSEQ_1:1;
        hence thesis by A8,A9,XXREAL_0:1;
      end;
    end;
  end;
  given l,r,i0 such that
A10: A = cell(l,r) and
A11: l.i0 < r.i0 or d = 1 & r.i0 < l.i0 and
A12: [l.i0,r.i0] is Gap of G.i0 and
A13: for i st i <> i0 holds l.i = r.i & l.i in G.i;
  set X = {i0};
  per cases by A11;
  suppose
A14: l.i0 < r.i0;
A15: card X = 1 by CARD_1:30;
    now
      let i;
      i in X iff i = i0 by TARSKI:def 1;
      hence i in X & l.i < r.i & [l.i,r.i] is Gap of G.i or
      not i in X & l.i = r.i & l.i in G.i by A12,A13,A14;
    end;
    hence thesis by A1,A10,A15,Th32;
  end;
  suppose
A16: d = 1 & r.i0 < l.i0;
    now
      let i;
A17:  1 <= i by FINSEQ_1:1;
A18:  i <= d by FINSEQ_1:1;
A19:  1 <= i0 by FINSEQ_1:1;
A20:  i0 <= d by FINSEQ_1:1;
A21:  i = 1 by A16,A17,A18,XXREAL_0:1;
      i0 = 1 by A16,A19,A20,XXREAL_0:1;
      hence r.i < l.i & [l.i,r.i] is Gap of G.i by A12,A16,A21;
    end;
    hence thesis by A10,A11,Th32;
  end;
end;

theorem
  cell(l,r) in cells(1,G) iff
  ex i0 st (l.i0 < r.i0 or d = 1 & r.i0 < l.i0) & [l.i0,r.i0] is Gap of G.i0 &
  for i st i <> i0 holds l.i = r.i & l.i in G.i
proof
  hereby
    assume cell(l,r) in cells(1,G);
    then consider l9,r9,i0 such that
A1: cell(l,r) = cell(l9,r9) and
A2: l9.i0 < r9.i0 or d = 1 & r9.i0 < l9.i0 and
A3: [l9.i0,r9.i0] is Gap of G.i0 and
A4: for i st i <> i0 holds l9.i = r9.i & l9.i in G.i by Th43;
A5: (for i holds l9.i <= r9.i) or for i holds r9.i < l9.i
    proof
      per cases by A2;
      suppose
A6:     l9.i0 < r9.i0;
        now
          let i;
          i = i0 or i <> i0;
          hence l9.i <= r9.i by A4,A6;
        end;
        hence thesis;
      end;
      suppose
A7:     d = 1 & r9.i0 < l9.i0;
        now
          let i;
A8:       1 <= i by FINSEQ_1:1;
A9:       i <= d by FINSEQ_1:1;
A10:      1 <= i0 by FINSEQ_1:1;
A11:      i0 <= d by FINSEQ_1:1;
A12:      i = 1 by A7,A8,A9,XXREAL_0:1;
          i0 = 1 by A7,A10,A11,XXREAL_0:1;
          hence r9.i < l9.i by A7,A12;
        end;
        hence thesis;
      end;
    end;
    then
A13: l = l9 by A1,Th31;
    r = r9 by A1,A5,Th31;
    hence ex i0 st (l.i0 < r.i0 or d = 1 & r.i0 < l.i0) &
    [l.i0,r.i0] is Gap of G.i0 &
    for i st i <> i0 holds l.i = r.i & l.i in G.i by A2,A3,A4,A13;
  end;
  thus thesis by Th43;
end;

theorem Th45:
  k <= d & k9 <= d & cell(l,r) in cells(k,G) & cell(l9,r9) in cells(k9,G) &
  cell(l,r) c= cell(l9,r9) implies for i holds l.i = l9.i & r.i = r9.i or
  l.i = l9.i & r.i = l9.i or l.i = r9.i & r.i = r9.i or
  l.i <= r.i & r9.i < l9.i & r9.i <= l.i & r.i <= l9.i
proof
  assume that
A1: k <= d and
A2: k9 <= d and
A3: cell(l,r) in cells(k,G) and
A4: cell(l9,r9) in cells(k9,G);
  assume
A5: cell(l,r) c= cell(l9,r9);
  let i;
  per cases by A2,A4,Th34;
  suppose
A6: for i holds l9.i < r9.i & [l9.i,r9.i] is Gap of G.i or
    l9.i = r9.i & l9.i in G.i;
    then
A7: for i holds l9.i <= r9.i;
    then
A8: l9.i <= l.i by A5,Th28;
A9: l.i <= r.i by A5,A7,Th28;
A10: r.i <= r9.i by A5,A7,Th28;
A11: l9.i <= r.i by A8,A9,XXREAL_0:2;
A12: l.i <= r9.i by A9,A10,XXREAL_0:2;
    thus thesis
    proof
      per cases by A6;
      suppose
A13:    [l9.i,r9.i] is Gap of G.i;
A14:    now
          assume that
A15:      l9.i <> l.i and
A16:      l.i <> r9.i;
A17:      l9.i < l.i by A8,A15,XXREAL_0:1;
A18:      l.i < r9.i by A12,A16,XXREAL_0:1;
          l.i in G.i by A1,A3,Th35;
          hence contradiction by A13,A17,A18,Th16;
        end;
        now
          assume that
A19:      l9.i <> r.i and
A20:      r.i <> r9.i;
A21:      l9.i < r.i by A11,A19,XXREAL_0:1;
A22:      r.i < r9.i by A10,A20,XXREAL_0:1;
          r.i in G.i by A1,A3,Th35;
          hence contradiction by A13,A21,A22,Th16;
        end;
        hence thesis by A9,A14,XXREAL_0:1;
      end;
      suppose l9.i = r9.i;
        hence thesis by A8,A10,A11,A12,XXREAL_0:1;
      end;
    end;
  end;
  suppose
A23: for i holds r9.i < l9.i & [l9.i,r9.i] is Gap of G.i;
    then
A24: r9.i < l9.i;
A25: [l9.i,r9.i] is Gap of G.i by A23;
    thus thesis
    proof
      per cases by A1,A3,Th34;
      suppose
A26:    for i holds r.i < l.i & [l.i,r.i] is Gap of G.i;
        then
A27:    r.i <= r9.i by A5,Th29;
A28:    l9.i <= l.i by A5,A26,Th29;
A29:    now
          assume l9.i <> l.i;
          then
A30:      l9.i < l.i by A28,XXREAL_0:1;
          l.i in G.i by A1,A3,Th35;
          hence contradiction by A24,A25,A30,Th16;
        end;
        now
          assume r.i <> r9.i;
          then
A31:      r.i < r9.i by A27,XXREAL_0:1;
          r.i in G.i by A1,A3,Th35;
          hence contradiction by A24,A25,A31,Th16;
        end;
        hence thesis by A29;
      end;
      suppose
A32:    for i holds l.i < r.i & [l.i,r.i] is Gap of G.i or
        l.i = r.i & l.i in G.i;
A33:    l.i in G.i by A1,A3,Th35;
        r.i in G.i by A1,A3,Th35;
        hence thesis by A24,A25,A32,A33,Th16;
      end;
    end;
  end;
end;

theorem Th46:
  k < k9 & k9 <= d & cell(l,r) in cells(k,G) & cell(l9,r9) in cells(k9,G) &
  cell(l,r) c= cell(l9,r9) implies
  ex i st l.i = l9.i & r.i = l9.i or l.i = r9.i & r.i = r9.i
proof
  assume that
A1: k < k9 and
A2: k9 <= d and
A3: cell(l,r) in cells(k,G) and
A4: cell(l9,r9) in cells(k9,G);
A5: k + 0 < d by A1,A2,XXREAL_0:2;
  assume
A6: cell(l,r) c= cell(l9,r9);
  consider X being Subset of Seg d such that
A7: card X = k and
A8: for i holds i in X & l.i < r.i & [l.i,r.i] is Gap of G.i or not i
  in X & l.i = r.i & l.i in G.i
  by A3,A5,Th33;
A9: d - k > 0 by A5,XREAL_1:20;
  card(Seg d \ X) = card Seg d - card X by CARD_2:44
    .= d - k by A7,FINSEQ_1:57;
  then consider i0 being set such that
A10: i0 in Seg d \ X by A9,CARD_1:27,XBOOLE_0:def 1;
  reconsider i0 as Element of Seg d by A10,XBOOLE_0:def 5;
  not i0 in X by A10,XBOOLE_0:def 5;
  then
A11: l.i0 = r.i0 by A8;
  per cases by A2,A3,A4,A5,A6,Th45;
  suppose l.i0 = l9.i0 & r.i0 = r9.i0;
    hence thesis by A11;
  end;
  suppose l.i0 = l9.i0 & r.i0 = l9.i0;
    hence thesis;
  end;
  suppose l.i0 = r9.i0 & r.i0 = r9.i0;
    hence thesis;
  end;
  suppose
A12: r9.i0 < l9.i0;
    assume
A13: for i holds (l.i <> l9.i or r.i <> l9.i) & (l.i <> r9.i or r.i <> r9.i);
    defpred P[Element of Seg d,Real] means
    l.$1 <= $2 & $2 <= r.$1 & r9.$1 < $2 & $2 < l9.$1;
A14: for i ex xi st P[i,xi]
    proof
      let i;
A15:  l.i in G.i by A3,A5,Th35;
A16:  r.i in G.i by A3,A5,Th35;
A17:  r9.i < l9.i by A2,A4,A12,Th34;
A18:  [l9.i,r9.i] is Gap of G.i by A2,A4,A12,Th34;
      per cases;
      suppose
A19:    r9.i < l.i & l.i < l9.i;
        take l.i;
        thus thesis by A8,A19;
      end;
      suppose
A20:    l.i <= r9.i;
A21:    l.i >= r9.i by A15,A17,A18,Th16;
        then
A22:    l.i = r9.i by A20,XXREAL_0:1;
        then r.i <> r9.i by A13;
        then l.i < r.i by A8,A22;
        then consider xi such that
A23:    l.i < xi and
A24:    xi < r.i by Th1;
        take xi;
        r.i <= l9.i by A16,A17,A18,Th16;
        hence thesis by A21,A23,A24,XXREAL_0:2;
      end;
      suppose
A25:    l9.i <= l.i;
        l9.i >= l.i by A15,A17,A18,Th16;
        then
A26:    l9.i = l.i by A25,XXREAL_0:1;
        l9.i >= r.i by A16,A17,A18,Th16;
        then l9.i = r.i by A8,A26;
        hence thesis by A13,A26;
      end;
    end;
    consider x being Function of Seg d,REAL such that
A27: for i holds P[i,x.i] from FUNCT_2:sch 3(A14);
    reconsider x as Element of REAL d by Def3;
A28: x in cell(l,r) by A27;
    for i st r9.i < l9.i holds r9.i < x.i & x.i < l9.i by A27;
    hence contradiction by A6,A12,A28,Th25;
  end;
end;

theorem Th47:
  for X,X9 being Subset of Seg d st cell(l,r) c= cell(l9,r9) &
  (for i holds (i in X & l.i < r.i & [l.i,r.i] is Gap of G.i) or
  (not i in X & l.i = r.i & l.i in G.i)) &
  (for i holds (i in X9 & l9.i < r9.i & [l9.i,r9.i] is Gap of G.i) or
  (not i in X9 & l9.i = r9.i & l9.i in G.i)) holds X c= X9 &
  (for i st i in X or not i in X9 holds l.i = l9.i & r.i = r9.i) &
  for i st not i in X & i in X9 holds
  l.i = l9.i & r.i = l9.i or l.i = r9.i & r.i = r9.i
proof
  let X,X9 be Subset of Seg d;
  assume
A1: cell(l,r) c= cell(l9,r9);
  assume
A2: for i holds i in X & l.i < r.i & [l.i,r.i] is Gap of G.i or
  not i in X & l.i = r.i & l.i in G.i;
  assume
A3: for i holds i in X9 & l9.i < r9.i & [l9.i,r9.i] is Gap of G.i or
  not i in X9 & l9.i = r9.i & l9.i in G.i;
A4: l in cell(l,r) by Th26;
A5: r in cell(l,r) by Th26;
A6: for i holds l9.i <= r9.i by A3;
  thus X c= X9
  proof
    let i be set;
    assume that
A7: i in X and
A8: not i in X9;
    reconsider i as Element of Seg d by A7;
A9: l.i < r.i by A2,A7;
A10: l9.i = r9.i by A3,A8;
A11: l9.i <= l.i by A1,A4,A6,Th24;
    r.i <= r9.i by A1,A5,A6,Th24;
    hence thesis by A9,A10,A11,XXREAL_0:2;
  end;
  set k = card X;
  set k9 = card X9;
A12: card Seg d = d by FINSEQ_1:57;
  then
A13: k <= d by NAT_1:43;
A14: k9 <= d by A12,NAT_1:43;
A15: cell(l,r) in cells(k,G) by A2,A13,Th33;
A16: cell(l9,r9) in cells(k9,G) by A3,A14,Th33;
  thus for i st i in X or not i in X9 holds l.i = l9.i & r.i = r9.i
  proof
    let i;
    assume
A17: i in X or not i in X9;
    l9.i <= r9.i by A3;
    then l.i = l9.i & r.i = r9.i or
    l.i = l9.i & r.i = l9.i or l.i = r9.i & r.i = r9.i by A1,A13,A14,A15,A16
,Th45;
    hence thesis by A2,A3,A17;
  end;
  thus for i st not i in X & i in X9 holds
  l.i = l9.i & r.i = l9.i or l.i = r9.i & r.i = r9.i
  proof
    let i;
    assume that
A18: not i in X and
A19: i in X9;
A20: l.i = r.i by A2,A18;
    l9.i < r9.i by A3,A19;
    hence thesis by A1,A13,A14,A15,A16,A20,Th45;
  end;
end;

definition
  let d,G,k;
  mode Cell of k,G is Element of cells(k,G);
end;

definition
  let d,G,k;
  mode Chain of k,G is Subset of cells(k,G);
end;

definition
  let d,G,k;
  func 0_(k,G) -> Chain of k,G equals
  {};
  coherence by SUBSET_1:1;
end;

definition
  let d,G;
  func Omega(G) -> Chain of d,G equals
  cells(d,G);
  coherence
  proof
    cells(d,G) c= cells(d,G);
    hence thesis;
  end;
end;

notation
  let d,G,k;
  let C1,C2 be Chain of k,G;
  synonym C1 + C2 for C1 \+\ C2;
end;

definition
  let d,G,k;
  let C1,C2 be Chain of k,G;
  redefine func C1 + C2 -> Chain of k,G;
  coherence
  proof
    C1 \+\ C2 c= cells(k,G);
    hence thesis;
  end;
end;

definition
  let d,G;
  func infinite-cell(G) -> Cell of d,G means
  :Def10:
  ex l,r st it = cell(l,r) & for i holds r.i < l.i & [l.i,r.i] is Gap of G.i;
  existence
  proof
    defpred P[Element of Seg d,Real] means
    $2 in G.$1 & for xi st xi in G.$1 holds xi <= $2;
A1: for i ex li st P[i,li] by Th11;
    consider l being Function of Seg d,REAL such that
A2: for i holds P[i,l.i] from FUNCT_2:sch 3(A1);
    reconsider l as Element of REAL d by Def3;
    defpred R[Element of Seg d,Real] means
    $2 in G.$1 & for xi st xi in G.$1 holds xi >= $2;
A3: for i ex ri st R[i,ri] by Th12;
    consider r being Function of Seg d,REAL such that
A4: for i holds R[i,r.i] from FUNCT_2:sch 3(A3);
    reconsider r as Element of REAL d by Def3;
A5: now
      let i;
      r.i in G.i by A4;
      then
A6:   r.i <= l.i by A2;
      now
        assume
A7:     l.i = r.i;
        consider x1,x2 be set such that
A8:     x1 in G.i and
A9:     x2 in G.i and
A10:    x1 <> x2 by ZFMISC_1:def 10;
        reconsider x1,x2 as Real by A8,A9;
A11:    r.i <= x1 by A4,A8;
A12:    x1 <= l.i by A2,A8;
A13:    r.i <= x2 by A4,A9;
A14:    x2 <= l.i by A2,A9;
        x1 = l.i by A7,A11,A12,XXREAL_0:1;
        hence contradiction by A7,A10,A13,A14,XXREAL_0:1;
      end;
      hence r.i < l.i by A6,XXREAL_0:1;
    end;
A15: now
      let i;
A16:  l.i in G.i by A2;
A17:  r.i in G.i by A4;
A18:  r.i < l.i by A5;
      for xi st xi in G.i holds not (l.i < xi or xi < r.i) by A2,A4;
      hence r.i < l.i & [l.i,r.i] is Gap of G.i by A16,A17,A18,Th16;
    end;
    then reconsider A = cell(l,r) as Cell of d,G by Th33;
    take A,l,r;
    thus thesis by A15;
  end;
  uniqueness
  proof
    let A,A9 be Cell of d,G;
    given l,r such that
A19: A = cell(l,r) and
A20: for i holds r.i < l.i & [l.i,r.i] is Gap of G.i;
    given l9,r9 such that
A21: A9 = cell(l9,r9) and
A22: for i holds r9.i < l9.i & [l9.i,r9.i] is Gap of G.i;
    reconsider l,r,l9,r9 as Function of Seg d,REAL by Def3;
A23: now
      let i;
A24:  r.i < l.i by A20;
A25:  [l.i,r.i] is Gap of G.i by A20;
A26:  r9.i < l9.i by A22;
      [l9.i,r9.i] is Gap of G.i by A22;
      hence l.i = l9.i & r.i = r9.i by A24,A25,A26,Th22;
    end;
    then l = l9 by FUNCT_2:63;
    hence thesis by A19,A21,A23,FUNCT_2:63;
  end;
end;

theorem Th48:
  cell(l,r) is Cell of d,G implies
  (cell(l,r) = infinite-cell(G) iff for i holds r.i < l.i)
proof
  assume
A1: cell(l,r) is Cell of d,G;
  then reconsider A = cell(l,r) as Cell of d,G;
  hereby
    assume cell(l,r) = infinite-cell(G);
    then consider l9,r9 such that
A2: cell(l,r) = cell(l9,r9) and
A3: for i holds r9.i < l9.i & [l9.i,r9.i] is Gap of G.i by Def10;
A4: l = l9 by A2,A3,Th31;
    r = r9 by A2,A3,Th31;
    hence for i holds r.i < l.i by A3,A4;
  end;
  set i0 = the Element of Seg d;
  assume for i holds r.i < l.i;
  then
A5: r.i0 < l.i0;
A6: A = cell(l,r);
  for i holds r.i < l.i & [l.i,r.i] is Gap of G.i by A1,A5,Th34;
  hence thesis by A6,Def10;
end;

theorem Th49:
  cell(l,r) = infinite-cell(G) iff
  for i holds r.i < l.i & [l.i,r.i] is Gap of G.i
proof
  hereby
    assume cell(l,r) = infinite-cell(G);
    then consider l9,r9 such that
A1: cell(l,r) = cell(l9,r9) and
A2: for i holds r9.i < l9.i & [l9.i,r9.i] is Gap of G.i by Def10;
A3: l = l9 by A1,A2,Th31;
    r = r9 by A1,A2,Th31;
    hence for i holds r.i < l.i & [l.i,r.i] is Gap of G.i by A2,A3;
  end;
  assume
A4: for i holds r.i < l.i & [l.i,r.i] is Gap of G.i;
  then cell(l,r) is Cell of d,G by Th33;
  hence thesis by A4,Def10;
end;

scheme ChainInd { d()->non zero Element of NAT, G()->Grating of d(),
  k()->Element of NAT, C()->Chain of k(),G(), P[set] } : P[C()]
provided
A1: P[0_(k(),G())] and
A2: for A being Cell of k(),G() st A in C() holds P[{A}] and
A3: for C1,C2 being Chain of k(),G() st C1 c= C() & C2 c= C() &
P[C1] & P[C2] holds P[C1 + C2]
proof
A4: C() is finite;
A5: P[{}] by A1;
A6: for x,B being set st x in C() & B c= C() & P[B] holds P[B \/ {x}]
  proof
    let A,C1 be set;
    assume that
A7: A in C() and
A8: C1 c= C() and
A9: P[C1];
    reconsider A9 = A as Cell of k(),G() by A7;
    reconsider C19 = C1 as Chain of k(),G() by A8,XBOOLE_1:1;
    per cases;
    suppose A in C1;
      then {A} c= C1 by ZFMISC_1:31;
      hence thesis by A9,XBOOLE_1:12;
    end;
    suppose
A10:  not A in C1;
      now
        let A9 be set;
        assume
A11:    A9 in C1 /\ {A};
        then
A12:    A9 in C1 by XBOOLE_0:def 4;
        A9 in {A} by A11,XBOOLE_0:def 4;
        hence contradiction by A10,A12,TARSKI:def 1;
      end;
      then C1 /\ {A} = {} by XBOOLE_0:def 1;
      then
A13:  C19 + {A9} = C1 \/ {A} \ {} by XBOOLE_1:101
        .= C1 \/ {A};
A14:  P[{A9}] by A2,A7;
      {A} c= C() by A7,ZFMISC_1:31;
      hence thesis by A3,A8,A9,A13,A14;
    end;
  end;
  thus P[C()] from FINSET_1:sch 2(A4,A5,A6);
end;

:: the boundary operator

definition
  let d,G,k;
  let A be Cell of k,G;
  func star A -> Chain of (k + 1),G equals
  { B where B is Cell of (k + 1),G : A c= B };
  coherence
  proof
    defpred P[set] means A c= $1;
    { B where B is Cell of (k + 1),G : P[B] } c= cells(k + 1,G) from
    FRAENKEL:sch 10;
    hence thesis;
  end;
end;

theorem Th50:
  for A being Cell of k,G, B being Cell of (k + 1),G holds
  B in star A iff A c= B
proof
  let A be Cell of k,G, B be Cell of (k + 1),G;
  defpred P[set] means A c= $1;
A1: star A = { B9 where B9 is Cell of (k + 1),G : P[B9] };
  thus B in star A iff P[B] from LMOD_7:sch 7(A1);
end;

definition
  let d,G,k;
  let C be Chain of (k + 1),G;
  func del C -> Chain of k,G equals
  { A where A is Cell of k,G : k + 1 <= d & card(star A /\ C) is odd };
  coherence
  proof
    defpred P[Cell of k,G] means k + 1 <= d & card(star $1 /\ C) is odd;
    { A where A is Cell of k,G : P[A] } c= cells(k,G) from FRAENKEL:sch 10;
    hence thesis;
  end;
end;

notation
  let d,G,k;
  let C be Chain of (k + 1),G;
  synonym .C for del C;
end;

definition
  let d,G,k;
  let C be Chain of (k + 1),G, C9 be Chain of k,G;
  pred C9 bounds C means
  C9 = del C;
end;

theorem Th51:
  for A being Cell of k,G, C being Chain of (k + 1),G holds
  A in del C iff k + 1 <= d & card(star A /\ C) is odd
proof
  let A be Cell of k,G, C be Chain of (k + 1),G;
  defpred P[Cell of k,G] means k + 1 <= d & card(star $1 /\ C) is odd;
A1: del C = { A9 where A9 is Cell of k,G : P[A9] };
  thus A in del C iff P[A] from LMOD_7:sch 7(A1);
end;

theorem Th52:
  k + 1 > d implies for C being Chain of (k + 1),G holds del C = 0_(k,G)
proof
  assume
A1: k + 1 > d;
  let C be Chain of (k + 1),G;
  for A being set holds not A in del C by A1,Th51;
  hence thesis by XBOOLE_0:def 1;
end;

theorem Th53:
  k + 1 <= d implies for A being Cell of k,G, B being Cell of (k + 1),G holds
  A in del {B} iff A c= B
proof
  assume
A1: k + 1 <= d;
  let A be Cell of k,G, B be Cell of (k + 1),G;
  set X = star A /\ {B};
  card X is odd iff B in star A
  proof
    per cases;
    suppose
A2:   B in star A;
      now
        let B9 be set;
        B9 in {B} iff B9 = B by TARSKI:def 1;
        hence B9 in X iff B9 = B by A2,XBOOLE_0:def 4;
      end;
      then X = {B} by TARSKI:def 1;
      then card X = 2* 0 + 1 by CARD_1:30;
      hence thesis by A2;
    end;
    suppose
A3:   not B in star A;
      now
        let B9 be set;
        B9 = B or not B9 in {B} by TARSKI:def 1;
        hence not B9 in X by A3,XBOOLE_0:def 4;
      end;
      then card X = 2* 0 by CARD_1:27,XBOOLE_0:def 1;
      hence thesis by A3;
    end;
  end;
  hence thesis by A1,Th50,Th51;
end;

:: lemmas

theorem Th54:
  d = d9 + 1 implies for A being Cell of d9,G holds card(star A) = 2
proof
  assume
A1: d = d9 + 1;
  then
A2: d9 < d by NAT_1:13;
  let A be Cell of d9,G;
  consider l,r,i0 such that
A3: A = cell(l,r) and
A4: l.i0 = r.i0 and
A5: l.i0 in G.i0 and
A6: for i st i <> i0 holds l.i < r.i & [l.i,r.i] is Gap of G.i by A1,Th41;
A7: now
    let i;
    i = i0 or i <> i0;
    hence l.i <= r.i by A4,A6;
  end;
  ex B1,B2 being set st B1 in star A & B2 in star A & B1 <> B2 &
  for B being set st B in star A holds B = B1 or B = B2
  proof
    ex l1,r1 st [l1.i0,r1.i0] is Gap of G.i0 & r1.i0 = l.i0 &
    ((l1.i0 < r1.i0 & for i st i <> i0 holds l1.i = l.i & r1.i = r.i) or
    for i holds r1.i < l1.i & [l1.i,r1.i] is Gap of G.i)
    proof
      consider l1i0 being Real such that
A8:   [l1i0,l.i0] is Gap of G.i0 by A5,Th19;
      per cases by A8,Th16;
      suppose
A9:     l1i0 < l.i0;
        defpred P[Element of Seg d,Real] means ($1 = i0 implies $2 = l1i0) &
        ($1 <> i0 implies $2 = l.$1);
A10:    for i ex li st P[i,li]
        proof
          let i;
          i = i0 or i <> i0;
          hence thesis;
        end;
        consider l1 being Function of Seg d,REAL such that
A11:    for i holds P[i,l1.i] from FUNCT_2:sch 3(A10);
        reconsider l1 as Element of REAL d by Def3;
        take l1,r;
        thus thesis by A4,A8,A9,A11;
      end;
      suppose
A12:    l.i0 < l1i0;
        consider l1,r1 such that
        cell(l1,r1) = infinite-cell(G) and
A13:    for i holds r1.i < l1.i & [l1.i,r1.i] is Gap of G.i by Def10;
        take l1,r1;
A14:    r1.i0 < l1.i0 by A13;
        [l1.i0,r1.i0] is Gap of G.i0 by A13;
        hence thesis by A8,A12,A13,A14,Th22;
      end;
    end;
    then consider l1,r1 such that
A15: [l1.i0,r1.i0] is Gap of G.i0 and
A16: r1.i0 = l.i0 and
A17: (l1.i0 < r1.i0 & for i st i <> i0 holds l1.i = l.i & r1.i = r.i)
    or for i holds r1.i < l1.i & [l1.i,r1.i] is Gap of G.i;
A18: now
      let i;
A19:  i
      <> i0 & l1.i = l.i & r1.i = r.i implies [l1.i,r1.i] is Gap of G.i by A6;
      i = i0 or i <> i0;
      hence [l1.i,r1.i] is Gap of G.i by A15,A17,A19;
    end;
A20: (for i holds l1.i < r1.i) or for i holds r1.i < l1.i
    proof
      per cases by A17;
      suppose
A21:    l1.i0 < r1.i0 & for i st i <> i0 holds l1.i = l.i & r1.i = r.i;
        now
          let i;
A22:      i <> i0 & l1.i = l.i & r1.i = r.i implies l1.i < r1.i by A6;
          i = i0 or i <> i0;
          hence l1.i < r1.i by A21,A22;
        end;
        hence thesis;
      end;
      suppose for i holds r1.i < l1.i & [l1.i,r1.i] is Gap of G.i;
        hence thesis;
      end;
    end;
    then reconsider B1 = cell(l1,r1) as Cell of d,G by A18,Th40;
    ex l2,r2 st [l2.i0,r2.i0] is Gap of G.i0 & l2.i0 = l.i0 &
    ((l2.i0 < r2.i0 & for i st i <> i0 holds l2.i = l.i & r2.i = r.i) or
    for i holds r2.i < l2.i & [l2.i,r2.i] is Gap of G.i)
    proof
      consider r2i0 being Real such that
A23:  [l.i0,r2i0] is Gap of G.i0 by A5,Th18;
      per cases by A23,Th16;
      suppose
A24:    l.i0 < r2i0;
        defpred P[Element of Seg d,Real] means ($1 = i0 implies $2 = r2i0) &
        ($1 <> i0 implies $2 = r.$1);
A25:    for i ex ri st P[i,ri]
        proof
          let i;
          i = i0 or i <> i0;
          hence thesis;
        end;
        consider r2 being Function of Seg d,REAL such that
A26:    for i holds P[i,r2.i] from FUNCT_2:sch 3(A25);
        reconsider r2 as Element of REAL d by Def3;
        take l,r2;
        thus thesis by A23,A24,A26;
      end;
      suppose
A27:    r2i0 < l.i0;
        consider l2,r2 such that
        cell(l2,r2) = infinite-cell(G) and
A28:    for i holds r2.i < l2.i & [l2.i,r2.i] is Gap of G.i by Def10;
        take l2,r2;
A29:    r2.i0 < l2.i0 by A28;
        [l2.i0,r2.i0] is Gap of G.i0 by A28;
        hence thesis by A23,A27,A28,A29,Th22;
      end;
    end;
    then consider l2,r2 such that
A30: [l2.i0,r2.i0] is Gap of G.i0 and
A31: l2.i0 = l.i0 and
A32: (l2.i0 < r2.i0 & for i st i <> i0 holds l2.i = l.i & r2.i = r.i)
    or for i holds r2.i < l2.i & [l2.i,r2.i] is Gap of G.i;
A33: now
      let i;
A34:  i
      <> i0 & l2.i = l.i & r2.i = r.i implies [l2.i,r2.i] is Gap of G.i by A6;
      i = i0 or i <> i0;
      hence [l2.i,r2.i] is Gap of G.i by A30,A32,A34;
    end;
    (for i holds l2.i < r2.i) or for i holds r2.i < l2.i
    proof
      per cases by A32;
      suppose
A35:    l2.i0 < r2.i0 & for i st i <> i0 holds l2.i = l.i & r2.i = r.i;
        now
          let i;
A36:      i <> i0 & l2.i = l.i & r2.i = r.i implies l2.i < r2.i by A6;
          i = i0 or i <> i0;
          hence l2.i < r2.i by A35,A36;
        end;
        hence thesis;
      end;
      suppose for i holds r2.i < l2.i & [l2.i,r2.i] is Gap of G.i;
        hence thesis;
      end;
    end;
    then reconsider B2 = cell(l2,r2) as Cell of d,G by A33,Th40;
    take B1,B2;
    A c= B1
    proof
      per cases by A17;
      suppose
A37:    l1.i0 < r1.i0 & for i st i <> i0 holds l1.i = l.i & r1.i = r.i;
A38:    now
          let i;
          i = i0 or i <> i0 & l1.i = l.i & r1.i = r.i by A37;
          hence l1.i <= r1.i by A6,A37;
        end;
        now
          let i;
          i = i0 or i <> i0 & l1.i = l.i & r1.i = r.i by A37;
          hence l1.i <= l.i & l.i <= r.i & r.i <= r1.i by A4,A16,A38;
        end;
        hence thesis by A3,A38,Th28;
      end;
      suppose for i holds r1.i < l1.i & [l1.i,r1.i] is Gap of G.i;
        hence thesis by A3,A4,A7,A16,Th30;
      end;
    end;
    hence B1 in star A by A1;
    A c= B2
    proof
      per cases by A32;
      suppose
A39:    l2.i0 < r2.i0 & for i st i <> i0 holds l2.i = l.i & r2.i = r.i;
A40:    now
          let i;
          i = i0 or i <> i0 & l2.i = l.i & r2.i = r.i by A39;
          hence l2.i <= r2.i by A6,A39;
        end;
        now
          let i;
          i = i0 or i <> i0 & l2.i = l.i & r2.i = r.i by A39;
          hence l2.i <= l.i & l.i <= r.i & r.i <= r2.i by A4,A31,A40;
        end;
        hence thesis by A3,A40,Th28;
      end;
      suppose for i holds r2.i < l2.i & [l2.i,r2.i] is Gap of G.i;
        hence thesis by A3,A7,A31,Th30;
      end;
    end;
    hence B2 in star A by A1;
A41: l1 <> l2 by A16,A17,A31;
    (for i holds l1.i <= r1.i) or for i holds r1.i < l1.i by A20;
    hence B1 <> B2 by A41,Th31;
    let B be set;
    assume
A42: B in star A;
    then reconsider B as Cell of d,G by A1;
    consider l9,r9 such that
A43: B = cell(l9,r9) and
A44: for i holds [l9.i,r9.i] is Gap of G.i and
A45: (for i holds l9.i < r9.i) or for i holds r9.i < l9.i by Th39;
A46: [l9.i0,r9.i0] is Gap of G.i0 by A44;
A47: A c= B by A42,Th50;
    per cases by A45;
    suppose
A48:  for i holds l9.i < r9.i;
A49:  now
        let i;
        assume
A50:    i <> i0;
        l9.i < r9.i by A48;
        then l.i = l9.i & r.i = r9.i or
        l.i = l9.i & r.i = l9.i or l.i = r9.i & r.i = r9.i
        by A2,A3,A43,A47,Th45;
        hence l9.i = l.i & r9.i = r.i by A6,A50;
      end;
      thus thesis
      proof
A51:    l9.i0 < r9.i0 by A48;
        per cases by A2,A3,A4,A43,A47,A51,Th45;
        suppose
A52:      l.i0 = r9.i0 & r.i0 = r9.i0;
          then
A53:      l9.i0 = l1.i0 by A15,A16,A46,Th21;
          reconsider l9,r9,l1,r1 as Function of Seg d,REAL by Def3;
A54:      now
            let i;
A55:        l1.i0 < l.i0 by A48,A52,A53;
            then i = i0 or i <> i0 & l9.i = l.i & l1.i = l.i by A16,A17,A49;
            hence l9.i = l1.i by A15,A16,A46,A52,Th21;
            i = i0 or i <> i0 & r9.i = r.i & r1.i = r.i by A16,A17,A49,A55;
            hence r9.i = r1.i by A16,A52;
          end;
          then l9 = l1 by FUNCT_2:63;
          hence thesis by A43,A54,FUNCT_2:63;
        end;
        suppose
A56:      l.i0 = l9.i0 & r.i0 = l9.i0;
          then
A57:      r9.i0 = r2.i0 by A30,A31,A46,Th20;
          reconsider l9,r9,l2,r2 as Function of Seg d,REAL by Def3;
A58:      now
            let i;
A59:        l.i0 < r2.i0 by A48,A56,A57;
            then i = i0 or i <> i0 & r9.i = r.i & r2.i = r.i by A31,A32,A49;
            hence r9.i = r2.i by A30,A31,A46,A56,Th20;
            i = i0 or i <> i0 & l9.i = l.i & l2.i = l.i by A31,A32,A49,A59;
            hence l9.i = l2.i by A31,A56;
          end;
          then l9 = l2 by FUNCT_2:63;
          hence thesis by A43,A58,FUNCT_2:63;
        end;
      end;
    end;
    suppose
A60:  for i holds r9.i < l9.i;
      consider i1 such that
A61:  l.i1 = l9.i1 & r.i1 = l9.i1 or l.i1 = r9.i1 & r.i1 = r9.i1
      by A2,A3,A43,A47,Th46;
A62:  i0 = i1 by A6,A61;
      thus thesis
      proof
        per cases by A61,A62;
        suppose
A63:      l.i0 = r9.i0 & r.i0 = r9.i0;
          then l9.i0 = l1.i0 by A15,A16,A46,Th21;
          then B1 = infinite-cell(G) by A16,A17,A60,A63,Th48;
          hence thesis by A43,A60,Th48;
        end;
        suppose
A64:      l.i0 = l9.i0 & r.i0 = l9.i0;
          then r9.i0 = r2.i0 by A30,A31,A46,Th20;
          then B2 = infinite-cell(G) by A31,A32,A60,A64,Th48;
          hence thesis by A43,A60,Th48;
        end;
      end;
    end;
  end;
  hence thesis by Th5;
end;

theorem Th55:
  for G being Grating of d, B being Cell of (0 + 1),G holds card(del {B}) = 2
proof
A1: 0 + 1 <= d by Def2;
  let G be Grating of d, B be Cell of (0 + 1),G;
  consider l,r,i0 such that
A2: B = cell(l,r) and
A3: l.i0 < r.i0 or d = 1 & r.i0 < l.i0 and
A4: [l.i0,r.i0] is Gap of G.i0 and
A5: for i st i <> i0 holds l.i = r.i & l.i in G.i by Th43;
  ex A1,A2 being set st A1 in del {B} & A2 in del {B} & A1 <> A2 &
  for A being set st A in del {B} holds A = A1 or A = A2
  proof
    for i holds l.i in G.i & r.i in G.i by A1,A2,Th35;
    then reconsider A1 = cell(l,l), A2 = cell(r,r) as Cell of 0,G by Th38;
    take A1,A2;
A6: A1 = {l} by Th27;
A7: A2 = {r} by Th27;
A8: l in B by A2,Th26;
A9: r in B by A2,Th26;
A10: {l} c= B by A8,ZFMISC_1:31;
    {r} c= B by A9,ZFMISC_1:31;
    hence A1 in del {B} & A2 in del {B} by A1,A6,A7,A10,Th53;
    thus A1 <> A2 by A3,A6,A7,ZFMISC_1:3;
    let A be set;
    assume
A11: A in del {B};
    then reconsider A as Cell of 0,G;
A12: A c= B by A1,A11,Th53;
    consider x such that
A13: A = cell(x,x) and
A14: for i holds x.i in G.i by Th37;
A15: x in A by A13,Th26;
    per cases by A3;
    suppose
A16:  l.i0 < r.i0;
A17:  now
        let i;
        i = i0 or i <> i0;
        hence l.i <= r.i by A5,A16;
      end;
A18:  x.i0 in G.i0 by A14;
A19:  l.i0 <= x.i0 by A2,A12,A15,A17,Th24;
A20:  x.i0 <= r.i0 by A2,A12,A15,A17,Th24;
A21:  not (l.i0 < x.i0 & x.i0 < r.i0) by A4,A18,Th16;
A22:  now
        let i;
        assume i <> i0;
        then
A23:    l.i = r.i by A5;
A24:    l.i <= x.i by A2,A12,A15,A17,Th24;
        x.i <= r.i by A2,A12,A15,A17,Th24;
        hence x.i = l.i & x.i = r.i by A23,A24,XXREAL_0:1;
      end;
      thus thesis
      proof
        per cases by A19,A20,A21,XXREAL_0:1;
        suppose
A25:      x.i0 = l.i0;
          reconsider x,l as Function of Seg d,REAL by Def3;
          now
            let i;
            i = i0 or i <> i0;
            hence x.i = l.i by A22,A25;
          end;
          then x = l by FUNCT_2:63;
          hence thesis by A13;
        end;
        suppose
A26:      x.i0 = r.i0;
          reconsider x,r as Function of Seg d,REAL by Def3;
          now
            let i;
            i = i0 or i <> i0;
            hence x.i = r.i by A22,A26;
          end;
          then x = r by FUNCT_2:63;
          hence thesis by A13;
        end;
      end;
    end;
    suppose
A27:  d = 1 & r.i0 < l.i0;
A28:  for i holds i = i0
      proof
        let i;
A29:    1 <= i by FINSEQ_1:1;
A30:    i <= d by FINSEQ_1:1;
A31:    1 <= i0 by FINSEQ_1:1;
A32:    i0 <= d by FINSEQ_1:1;
        i = 1 by A27,A29,A30,XXREAL_0:1;
        hence thesis by A27,A31,A32,XXREAL_0:1;
      end;
      consider i1 such that
      r.i1 < l.i1 and
A33:  x.i1 <= r.i1 or l.i1 <= x.i1 by A2,A12,A15,A27,Th25;
A34:  i1 = i0 by A28;
A35:  x.i0 in G.i0 by A14;
      then
A36:  not x.i0 < r.i0 by A4,A27,Th16;
A37:  not l.i0 < x.i0 by A4,A27,A35,Th16;
      thus thesis
      proof
        per cases by A33,A34,A36,A37,XXREAL_0:1;
        suppose
A38:      x.i0 = r.i0;
          reconsider x,r as Function of Seg d,REAL by Def3;
          now
            let i;
            i = i0 by A28;
            hence x.i = r.i by A38;
          end;
          then x = r by FUNCT_2:63;
          hence thesis by A13;
        end;
        suppose
A39:      x.i0 = l.i0;
          reconsider x,l as Function of Seg d,REAL by Def3;
          now
            let i;
            i = i0 by A28;
            hence x.i = l.i by A39;
          end;
          then x = l by FUNCT_2:63;
          hence thesis by A13;
        end;
      end;
    end;
  end;
  hence thesis by Th5;
end;

:: theorems

theorem
  Omega(G) = 0_(d,G)` & 0_(d,G) = (Omega(G))`
proof
  Omega(G) = 0_(d,G)`;
  hence thesis;
end;

theorem
  for C being Chain of k,G holds C + 0_(k,G) = C;

theorem Th58:
  for C being Chain of d,G holds C` = C + Omega(G)
proof
  let C be Chain of d,G;
  C /\ cells(d,G) = C by XBOOLE_1:28;
  hence thesis by XBOOLE_1:100;
end;

theorem Th59:
  del 0_(k + 1,G) = 0_(k,G)
proof
  now
    let A be Cell of k,G;
    card(star A /\ 0_(k + 1,G)) = 2* 0;
    hence A in del 0_(k + 1,G) iff A in 0_(k,G) by Th51;
  end;
  hence thesis by SUBSET_1:3;
end;

theorem Th60:
  for G being Grating of d9 + 1 holds del Omega(G) = 0_(d9,G)
proof
  let G be Grating of d9 + 1;
  now
    let A be Cell of d9,G;
    star A /\ Omega(G) = star A by XBOOLE_1:28;
    then card(star A /\ Omega(G)) = 2* 1 by Th54;
    hence A in del Omega(G) iff A in 0_(d9,G) by Th51;
  end;
  hence thesis by SUBSET_1:3;
end;

theorem Th61:
  for C1,C2 being Chain of (k + 1),G holds del(C1 + C2) = del C1 + del C2
proof
  let C1,C2 be Chain of (k + 1),G;
  now
    let A be Cell of k,G;
    A1: star
 A /\ (C1 \+\ C2) = (star A /\ C1) \+\ (star A /\ C2) by XBOOLE_1:112;
A2: A in del(C1 + C2) iff k + 1 <= d & card(star A /\ (C1 \+\ C2)) is odd
    by Th51;
A3: A in del(C1) iff k + 1 <= d & card(star A /\ C1) is odd by Th51;
    A in del(C2) iff k + 1 <= d & card(star A /\ C2) is odd by Th51;
    hence A in del(C1 + C2) iff A in del C1 + del C2 by A1,A2,A3,Th8,XBOOLE_0:1
;
  end;
  hence thesis by SUBSET_1:3;
end;

theorem Th62:
  for G being Grating of d9 + 1, C being Chain of (d9 + 1),G holds
  del C` = del C
proof
  let G be Grating of d9 + 1, C be Chain of (d9 + 1),G;
  thus del C` = del(C + Omega(G)) by Th58
    .= del C + del Omega(G) by Th61
    .= del C + 0_(d9,G) by Th60
    .= del C;
end;

theorem Th63:
  for C being Chain of (k + 1 + 1),G holds del (del C) = 0_(k,G)
proof
  let C be Chain of (k + 1 + 1),G;
  per cases;
  suppose
A1: k + 1 + 1 <= d;
    then
A2: k + 1 < d by NAT_1:13;
    then
A3: k < d by NAT_1:13;
A4: for C being Cell of (k + 1 + 1),G, l,r
    st C = cell(l,r) & for i holds l.i <= r.i holds del (del {C}) = 0_(k,G)
    proof
      let C be Cell of (k + 1 + 1),G, l,r;
      assume that
A5:   C = cell(l,r) and
A6:   for i holds l.i <= r.i;
      now
        let A be set;
        assume
A7:     A in del (del {C});
        then reconsider A as Cell of k,G;
        set BB = star A /\ del {C};
A8:     now
          let B be Cell of (k + 1),G;
          B in BB iff B in star A & B in del {C} by XBOOLE_0:def 4;
          hence B in BB iff A c= B & B c= C by A1,Th50,Th53;
        end;
A9:     card BB is odd by A7,Th51;
        consider B being set such that
A10:    B in BB by A9,CARD_1:27,XBOOLE_0:def 1;
        reconsider B as Cell of (k + 1),G by A10;
A11:    A c= B by A8,A10;
        B c= C by A8,A10;
        then
A12:    A c= C by A11,XBOOLE_1:1;
        set i0 = the Element of Seg d;
        l.i0 <= r.i0 by A6;
        then consider Z being Subset of Seg d such that
A13:    card Z = k + 1 + 1 and
A14:    for i holds i in Z & l.i < r.i & [l.i,r.i] is Gap of G.i or not
        i in Z & l.i = r.i & l.i in G.i
        by A1,A5,Th33;
        consider l9,r9 such that
A15:    A = cell(l9,r9) and
A16:    (ex X being Subset of Seg d st card X = k & for i holds (i in X &
l9.i < r9.i & [l9.i,r9.i] is Gap of G.i) or (not i in X & l9.i = r9.i & l9.i in
        G.i)) or (k = d & for i holds r9.i < l9.i & [l9.i,r9.i] is Gap of G.i)
        by A3,Th32;
        l9.i0 <= r9.i0 by A5,A6,A12,A15,Th28;
        then consider X being Subset of Seg d such that
A17:    card X = k and
A18:    for i holds i in X & l9.i < r9.i & [l9.i,r9.i] is Gap of G.i or
        not i in X & l9.i = r9.i & l9.i in G.i
        by A16;
        ex B1,B2 being set st B1 in BB & B2 in BB & B1 <> B2 &
        for B being set st B in BB holds B = B1 or B = B2
        proof
A19:      X c= Z by A5,A12,A14,A15,A18,Th47;
          then card(Z \ X) = (k + (1 + 1)) - k by A13,A17,CARD_2:44
            .= 2;
          then consider i1,i2 being set such that
A20:      i1 in Z \ X and
A21:      i2 in Z \ X and
A22:      i1 <> i2 and
A23:      for i being set st i in Z \ X holds i = i1 or i = i2 by Th5;
A24:      i1 in Z by A20,XBOOLE_0:def 5;
A25:      i2 in Z by A21,XBOOLE_0:def 5;
A26:      not i1 in X by A20,XBOOLE_0:def 5;
A27:      not i2 in X by A21,XBOOLE_0:def 5;
          reconsider i1,i2 as Element of Seg d by A20,A21;
          set Y1 = X \/ {i1};
A28:      X c= Y1 by XBOOLE_1:7;
          {i1} c= Z by A24,ZFMISC_1:31;
          then
A29:      Y1 c= Z by A19,XBOOLE_1:8;
          defpred S[Element of Seg d,Real] means
          ($1 in Y1 implies $2 = l.$1) & (not $1 in Y1 implies $2 = l9.$1);
A30:      for i ex xi st S[i,xi]
          proof
            let i;
            i in Y1 or not i in Y1;
            hence thesis;
          end;
          consider l1 being Function of Seg d,REAL such that
A31:      for i holds S[i,l1.i] from FUNCT_2:sch 3(A30);
          defpred R[Element of Seg d,Real] means
          ($1 in Y1 implies $2 = r.$1) & (not $1 in Y1 implies $2 = r9.$1);
A32:      for i ex xi st R[i,xi]
          proof
            let i;
            i in Y1 or not i in Y1;
            hence thesis;
          end;
          consider r1 being Function of Seg d,REAL such that
A33:      for i holds R[i,r1.i] from FUNCT_2:sch 3(A32);
          reconsider l1,r1 as Element of REAL d by Def3;
A34:      for i holds l1.i <= r1.i
          proof
            let i;
l1.i = l.i & r1.i = r.i or l1.i = l9.i & r1.i = r9.i by A31,A33;
            hence thesis by A14,A18;
          end;
A35:      card Y1 = card X + card {i1} by A26,CARD_2:40,ZFMISC_1:50
            .= k + 1 by A17,CARD_1:30;
          for i holds i in Y1 & l1.i < r1.i & [l1.i,r1.i] is Gap of G.i or
          not i in Y1 & l1.i = r1.i & l1.i in G.i
          proof
            let i;
            per cases;
            suppose
A36:          i in Y1;
              then
A37:          l1.i = l.i by A31;
              r1.i = r.i by A33,A36;
              hence thesis by A14,A29,A36,A37;
            end;
            suppose
A38:          not i in Y1;
              then
A39:          l1.i = l9.i by A31;
A40:          r1.i = r9.i by A33,A38;
              not i in X by A28,A38;
              hence thesis by A18,A38,A39,A40;
            end;
          end;
          then reconsider B1 = cell(l1,r1) as Cell of (k + 1),G by A2,A35,Th33;
          set Y2 = X \/ {i2};
A41:      X c= Y2 by XBOOLE_1:7;
          {i2} c= Z by A25,ZFMISC_1:31;
          then
A42:      Y2 c= Z by A19,XBOOLE_1:8;
          defpred P[Element of Seg d,Real] means
          ($1 in Y2 implies $2 = l.$1) & (not $1 in Y2 implies $2 = l9.$1);
A43:      for i ex xi st P[i,xi]
          proof
            let i;
            i in Y2 or not i in Y2;
            hence thesis;
          end;
          consider l2 being Function of Seg d,REAL such that
A44:      for i holds P[i,l2.i] from FUNCT_2:sch 3(A43);
          defpred R[Element of Seg d,Real] means
          ($1 in Y2 implies $2 = r.$1) & (not $1 in Y2 implies $2 = r9.$1);
A45:      for i ex xi st R[i,xi]
          proof
            let i;
            i in Y2 or not i in Y2;
            hence thesis;
          end;
          consider r2 being Function of Seg d,REAL such that
A46:      for i holds R[i,r2.i] from FUNCT_2:sch 3(A45);
          reconsider l2,r2 as Element of REAL d by Def3;
A47:      card Y2 = card X + card {i2} by A27,CARD_2:40,ZFMISC_1:50
            .= k + 1 by A17,CARD_1:30;
          for i holds i in Y2 & l2.i < r2.i & [l2.i,r2.i] is Gap of G.i or
          not i in Y2 & l2.i = r2.i & l2.i in G.i
          proof
            let i;
            per cases;
            suppose
A48:          i in Y2;
              then
A49:          l2.i = l.i by A44;
              r2.i = r.i by A46,A48;
              hence thesis by A14,A42,A48,A49;
            end;
            suppose
A50:          not i in Y2;
              then
A51:          l2.i = l9.i by A44;
A52:          r2.i = r9.i by A46,A50;
              not i in X by A41,A50;
              hence thesis by A18,A50,A51,A52;
            end;
          end;
          then reconsider B2 = cell(l2,r2) as Cell of (k + 1),G by A2,A47,Th33;
          take B1,B2;
A53:      for i holds l1.i <= l9.i & l9.i <= r9.i & r9.i <= r1.i &
          l.i <= l1.i & l1.i <= r1.i & r1.i <= r.i
          proof
            let i;
            per cases;
            suppose
A54:          i in Y1;
              then
A55:          l1.i = l.i by A31;
              r1.i = r.i by A33,A54;
              hence thesis by A5,A6,A12,A15,A55,Th28;
            end;
            suppose
A56:          not i in Y1;
              then
A57:          l1.i = l9.i by A31;
              r1.i = r9.i by A33,A56;
              hence thesis by A5,A6,A12,A15,A57,Th28;
            end;
          end;
          then
A58:      A c= B1 by A15,Th28;
          B1 c= C by A5,A6,A53,Th28;
          hence B1 in BB by A8,A58;
A59:      for i holds l2.i <= l9.i & l9.i <= r9.i & r9.i <= r2.i &
          l.i <= l2.i & l2.i <= r2.i & r2.i <= r.i
          proof
            let i;
            per cases;
            suppose
A60:          i in Y2;
              then
A61:          l2.i = l.i by A44;
              r2.i = r.i by A46,A60;
              hence thesis by A5,A6,A12,A15,A61,Th28;
            end;
            suppose
A62:          not i in Y2;
              then
A63:          l2.i = l9.i by A44;
              r2.i = r9.i by A46,A62;
              hence thesis by A5,A6,A12,A15,A63,Th28;
            end;
          end;
          then
A64:      A c= B2 by A15,Th28;
          B2 c= C by A5,A6,A59,Th28;
          hence B2 in BB by A8,A64;
          i1 in {i1} by TARSKI:def 1;
          then
A65:      i1 in Y1 by XBOOLE_0:def 3;
A66:      not i1 in X by A20,XBOOLE_0:def 5;
          not i1 in {i2} by A22,TARSKI:def 1;
          then
A67:      not i1 in Y2 by A66,XBOOLE_0:def 3;
A68:      l1.i1 = l.i1 by A31,A65;
A69:      r1.i1 = r.i1 by A33,A65;
A70:      l2.i1 = l9.i1 by A44,A67;
A71:      r2.i1 = r9.i1 by A46,A67;
          l.i1 < r.i1 by A14,A24;
          then l1 <> l2 or r1 <> r2 by A18,A26,A68,A69,A70,A71;
          hence B1 <> B2 by A34,Th31;
          let B be set;
          assume
A72:      B in BB;
          then reconsider B as Cell of (k + 1),G;
A73:      A c= B by A8,A72;
A74:      B c= C by A8,A72;
          consider l99,r99 such that
A75:      B = cell(l99,r99) and
A76:      (ex Y being Subset of Seg d st card Y = k + 1 & for i holds (i in
Y & l99.i < r99.i & [l99.i,r99.i] is Gap of G.i) or (not i in Y & l99.i = r99.i
& l99.i in G.i)) or (k + 1 = d & for i holds r99.i < l99.i & [l99.i,r99.i] is
          Gap of G.i)
          by A2,Th32;
          l99.i0 <= r99.i0 by A5,A6,A74,A75,Th28;
          then consider Y being Subset of Seg d such that
A77:      card Y = k + 1 and
A78:      for i holds i in Y & l99.i < r99.i & [l99.i,r99.i] is Gap of G.i
          or not i in Y & l99.i = r99.i & l99.i in G.i
          by A76;
A79:      X c= Y by A15,A18,A73,A75,A78,Th47;
A80:      Y c= Z by A5,A14,A74,A75,A78,Th47;
          card(Y \ X) = (k + 1) - k by A17,A77,A79,CARD_2:44
            .= 1;
          then consider i9 being set such that
A81:      Y \ X = {i9} by CARD_2:42;
A82:      i9 in Y \ X by A81,TARSKI:def 1;
          then reconsider i9 as Element of Seg d;
A83:      i9 in Y by A82,XBOOLE_0:def 5;
          not i9 in X by A82,XBOOLE_0:def 5;
          then
A84:      i9 in Z \ X by A80,A83,XBOOLE_0:def 5;
A85:      Y = X \/ Y by A79,XBOOLE_1:12
            .= X \/ {i9} by A81,XBOOLE_1:39;
          per cases by A23,A84,A85;
          suppose
A86:        Y = Y1;
            reconsider l99,r99,l1,r1 as Function of Seg d,REAL by Def3;
A87:        now
              let i;
              i in Y or not i in Y;
              then l99.i = l.i & l1.i = l.i & r99.i = r.i & r1.i = r.i or
              l99.i = l9.i & l1.i = l9.i & r99.i = r9.i & r1.i = r9.i
              by A5,A14,A15,A18,A31,A33,A73,A74,A75,A78,A86,Th47;
              hence l99.i = l1.i & r99.i = r1.i;
            end;
            then l99 = l1 by FUNCT_2:63;
            hence thesis by A75,A87,FUNCT_2:63;
          end;
          suppose
A88:        Y = Y2;
            reconsider l99,r99,l2,r2 as Function of Seg d,REAL by Def3;
A89:        now
              let i;
              i in Y or not i in Y;
              then l99.i = l.i & l2.i = l.i & r99.i = r.i & r2.i = r.i or
              l99.i = l9.i & l2.i = l9.i & r99.i = r9.i & r2.i = r9.i
              by A5,A14,A15,A18,A44,A46,A73,A74,A75,A78,A88,Th47;
              hence l99.i = l2.i & r99.i = r2.i;
            end;
            then l99 = l2 by FUNCT_2:63;
            hence thesis by A75,A89,FUNCT_2:63;
          end;
        end;
        then card BB = 2* 1 by Th5;
        hence contradiction by A7,Th51;
      end;
      hence thesis by XBOOLE_0:def 1;
    end;
A90: for C1,C2 being Chain of (k + 1 + 1),G
    st del (del C1) = 0_(k,G) & del (del C2) = 0_(k,G) holds
    del (del(C1 + C2)) = 0_(k,G)
    proof
      let C1,C2 be Chain of (k + 1 + 1),G;
      assume that
A91:  del (del C1) = 0_(k,G) and
A92:  del (del C2) = 0_(k,G);
      thus del (del(C1 + C2)) = del (del C1 + del C2) by Th61
        .= 0_(k,G) + 0_(k,G) by A91,A92,Th61
        .= 0_(k,G);
    end;
    defpred P[Chain of k+1+1,G] means del (del $1) = 0_(k,G);
    del (del 0_(k + 1 + 1,G)) = del 0_(k + 1,G) by Th59
      .= 0_(k,G) by Th59;
    then
A93: P[0_(k+1+1,G)];
    for A being Cell of (k + 1 + 1),G holds del (del {A}) = 0_(k,G)
    proof
      let A be Cell of (k + 1 + 1),G;
      consider l,r such that
A94:  A = cell(l,r) and
A95:  (ex X being Subset of Seg d st card X = k + 1 + 1 & for i holds (
i in X & l.i < r.i & [l.i,r.i] is Gap of G.i) or (not i in X & l.i = r.i & l.i
in G.i)) or (k + 1 + 1 = d & for i holds r.i < l.i & [l.i,r.i] is Gap of G.i)
      by A1,Th32;
      per cases by A95;
      suppose ex X being Subset of Seg d st card X = k + 1 + 1 &
        for i holds i in X & l.i < r.i & [l.i,r.i] is Gap of G.i or
        not i in X & l.i = r.i & l.i in G.i;
        then for i holds l.i <= r.i;
        hence thesis by A4,A94;
      end;
      suppose
A96:    k + 1 + 1 = d & for i holds r.i < l.i & [l.i,r.i] is Gap of G.i;
        then
A97:    A = infinite-cell(G) by A94,Th49;
        set C = {A}`;
A98:    for A being Cell of k+1+1,G st A in C holds P[{A}]
        proof
          let A9 be Cell of (k + 1 + 1),G;
          assume A9 in C;
          then not A9 in {A} by XBOOLE_0:def 5;
          then
A99:      A9 <> infinite-cell(G) by A97,TARSKI:def 1;
          consider l9,r9 such that
A100:     A9 = cell(l9,r9) and
A101:     (ex X being Subset of Seg d st card X = k + 1 + 1 & for i holds (
i in X & l9.i < r9.i & [l9.i,r9.i] is Gap of G.i) or (not i in X & l9.i = r9.i
& l9.i in G.i)) or (k + 1 + 1 = d & for i holds r9.i < l9.i & [l9.i,r9.i] is
          Gap of G.i)
          by A1,Th32;
          per cases by A101;
          suppose ex X being Subset of Seg d st card X = k + 1 + 1 &
            for i holds i in X & l9.i < r9.i & [l9.i,r9.i] is Gap of G.i or
            not i in X & l9.i = r9.i & l9.i in G.i;
            then for i holds l9.i <= r9.i;
            hence thesis by A4,A100;
          end;
          suppose for i holds r9.i < l9.i & [l9.i,r9.i] is Gap of G.i;
            hence thesis by A99,A100,Th49;
          end;
        end;
A102:   for C1,C2 being Chain of k+1+1,G st C1 c= C & C2 c= C &
        P[C1] & P[C2] holds P[C1 + C2] by A90;
        P[C] from ChainInd(A93,A98,A102);
        hence thesis by A96,Th62;
      end;
    end;
    then
A103: for A being Cell of k+1+1,G st A in C holds P[{A}];
A104: for C1,C2 being Chain of k+1+1,G st C1 c= C & C2 c= C &
    P[C1] & P[C2] holds P[C1 + C2] by A90;
    thus P[C] from ChainInd(A93,A103,A104);
  end;
  suppose k + 1 + 1 > d;
    then del C = 0_(k + 1,G) by Th52;
    hence thesis by Th59;
  end;
end;

:: cycles

definition
  let d,G,k;
  mode Cycle of k,G -> Chain of k,G means
    :Def14:
    k = 0 & card it is even or
    ex k9 st k = k9 + 1 & ex C being Chain of (k9 + 1),G st C = it &
    del C = 0_(k9,G);
  existence
  proof
    per cases by NAT_1:6;
    suppose
A1:   k = 0;
      take 0_(k,G);
      thus thesis by A1;
    end;
    suppose ex k9 being Nat st k = k9 + 1;
      then consider k9 being Nat such that
A2:   k = k9 + 1;
      reconsider k9 as Element of NAT by ORDINAL1:def 12;
      take C9 = 0_(k,G);
      now
        take k9;
        thus k = k9 + 1 by A2;
        reconsider C = C9 as Chain of (k9 + 1),G by A2;
        take C;
        thus C = C9 & del C = 0_(k9,G) by A2,Th59;
      end;
      hence thesis;
    end;
  end;
end;

theorem Th64:
  for C being Chain of (k + 1),G holds
  C is Cycle of (k + 1),G iff del C = 0_(k,G)
proof
  let C be Chain of (k + 1),G;
  hereby
    assume C is Cycle of (k + 1),G;
    then ex k9 st ( k + 1 = k9 + 1)&( ex C9 being Chain of (k9 + 1),
    G st C9 = C & del C9 = 0_(k9,G)) by Def14;
    hence del C = 0_(k,G);
  end;
  thus thesis by Def14;
end;

theorem
  k > d implies for C being Chain of k,G holds C is Cycle of k,G
proof
  assume
A1: k > d;
  let C be Chain of k,G;
  consider k9 being Nat such that
A2: k = k9 + 1 by A1,NAT_1:6;
  reconsider k9 as Element of NAT by ORDINAL1:def 12;
  reconsider C9 = C as Chain of (k9 + 1),G by A2;
  del C9 = 0_(k9,G) by A1,A2,Th52;
  hence thesis by A2,Def14;
end;

theorem Th66:
  for C being Chain of 0,G holds C is Cycle of 0,G iff card C is even
proof
  let C be Chain of 0,G;
  hereby
    assume C is Cycle of 0,G;
    then 0 = 0 & card C is even or
    ex k9 st 0 = k9 + 1 & ex C9 being Chain of (k9 + 1),G st C9 = C &
    del C9 = 0_(k9,G) by Def14;
    hence card C is even;
  end;
  thus thesis by Def14;
end;

definition
  let d,G,k;
  let C be Cycle of (k + 1),G;
  redefine func del C equals
  0_(k,G);
  compatibility by Th64;
end;

definition
  let d,G,k;
  redefine func 0_(k,G) -> Cycle of k,G;
  coherence
  proof
    per cases by NAT_1:6;
    suppose
A1:   k = 0;
      card {} = 2* 0;
      hence thesis by A1,Def14;
    end;
    suppose ex k9 being Nat st k = k9 + 1;
      then consider k9 being Nat such that
A2:   k = k9 + 1;
      reconsider k9 as Element of NAT by ORDINAL1:def 12;
      del 0_(k9 + 1,G) = 0_(k9,G) by Th59;
      hence thesis by A2,Def14;
    end;
  end;
end;

definition
  let d,G;
  redefine func Omega(G) -> Cycle of d,G;
  coherence
  proof
    consider d9 being Nat such that
A1: d = d9 + 1 by NAT_1:6;
    reconsider d9 as Element of NAT by ORDINAL1:def 12;
    reconsider G as Grating of d9 + 1 by A1;
    del Omega(G) = 0_(d9,G) by Th60;
    hence thesis by A1,Def14;
  end;
end;

definition
  let d,G,k;
  let C1,C2 be Cycle of k,G;
  redefine func C1 + C2 -> Cycle of k,G;
  coherence
  proof
    per cases by NAT_1:6;
    suppose
A1:   k = 0;
      then
A2:   card C1 is even by Th66;
      card C2 is even by A1,Th66;
      then card(C1 + C2) is even by A2,Th8;
      hence C1 + C2 is Cycle of k,G by A1,Th66;
    end;
    suppose ex k9 being Nat st k = k9 + 1;
      then consider k9 being Nat such that
A3:   k = k9 + 1;
      reconsider k9 as Element of NAT by ORDINAL1:def 12;
      reconsider C1,C2 as Cycle of (k9 + 1),G by A3;
A4:   del C1 = 0_(k9,G);
      del C2 = 0_(k9,G);
      then del(C1 + C2) = 0_(k9,G) + 0_(k9,G) by A4,Th61
        .= 0_(k9,G);
      hence thesis by A3,Th64;
    end;
  end;
end;

theorem
  for C being Cycle of d,G holds C` is Cycle of d,G
proof
  let C be Cycle of d,G;
  consider d9 being Nat such that
A1: d = d9 + 1 by NAT_1:6;
  reconsider d9 as Element of NAT by ORDINAL1:def 12;
  reconsider G as Grating of d9 + 1 by A1;
  reconsider C as Cycle of (d9 + 1),G by A1;
  del C = 0_(d9,G);
  then del C` = 0_(d9,G) by Th62;
  hence thesis by A1,Th64;
end;

definition
  let d,G,k;
  let C be Chain of (k + 1),G;
  redefine func del C -> Cycle of k,G;
  coherence
  proof
    per cases by NAT_1:6;
    suppose
A1:   k = 0;
      defpred P[Chain of (k + 1),G] means del $1 is Cycle of k,G;
      del 0_(k + 1,G) = 0_(k,G);
      then
A2:   P[0_(k + 1,G)];
      now
        let B be Cell of (0 + 1),G;
        assume B in C;
        card(del {B}) = 2* 1 by Th55;
        hence del {B} is Cycle of 0,G by Def14;
      end;
      then
A3:   for A being Cell of (k + 1),G st A in C holds P[{A}] by A1;
A4:   for C1,C2 being Chain of (k + 1),G st C1 c= C & C2 c= C &
      P[C1] & P[C2] holds P[C1 + C2]
      proof
        let C1,C2 be Chain of (k + 1),G;
        assume that C1 c= C and C2 c= C and
A5:     P[C1] and
A6:     P[C2];
        reconsider C19 = del C1, C29 = del C2 as Cycle of k,G by A5,A6;
        del(C1 + C2) = C19 + C29 by Th61;
        hence thesis;
      end;
      thus P[C] from ChainInd(A2,A3,A4);
    end;
    suppose ex k9 being Nat st k = k9 + 1;
      then consider k9 being Nat such that
A7:   k = k9 + 1;
      reconsider k9 as Element of NAT by ORDINAL1:def 12;
      reconsider C as Chain of (k9 + 1 + 1),G by A7;
      del (del C) = 0_(k9,G) by Th63;
      hence thesis by A7,Th64;
    end;
  end;
end;

begin :: groups and homomorphisms

definition
  let d,G,k;
  func Chains(k,G) -> strict AbGroup means
  :Def16:
  the carrier of it = bool(cells(k,G)) & 0.it = 0_(k,G) &
  for A,B being Element of it, A9,B9 being Chain of k,G
  st A = A9 & B = B9 holds A + B = A9 + B9;
  existence
  proof
    deffunc f(Chain of k,G, Chain of k,G) = $1 + $2;
    consider op being BinOp of bool(cells(k,G)) such that
A1: for A,B being Chain of k,G holds op.(A,B) = f(A,B) from BINOP_1:sch 4;
    set ch = addLoopStr(#bool(cells(k,G)),op,0_(k,G)#);
A2: ch is add-associative
    proof
      let A,B,C be Element of ch;
      reconsider A9 = A, B9 = B, C9 = C as Chain of k,G;
      thus (A + B) + C = op.(A9 + B9,C) by A1
        .= (A9 + B9) + C9 by A1
        .= A9 + (B9 + C9) by XBOOLE_1:91
        .= op.(A,B9 + C9) by A1
        .= A + (B + C) by A1;
    end;
A3: ch is right_zeroed
    proof
      let A be Element of ch;
      reconsider A9 = A as Chain of k,G;
      thus A + 0.ch = A9 + 0_(k,G) by A1
        .= A;
    end;
A4: ch is right_complementable
    proof
      let A be Element of ch;
      reconsider A9 = A as Chain of k,G;
      take A;
      thus A + A = A9 + A9 by A1
        .= 0.ch by XBOOLE_1:92;
    end;
    ch is Abelian
    proof
      let A,B be Element of ch;
      reconsider A9 = A, B9 = B as Chain of k,G;
      thus A + B = A9 + B9 by A1
        .= B + A by A1;
    end;
    then reconsider ch as strict AbGroup by A2,A3,A4;
    take ch;
    thus the carrier of ch = bool(cells(k,G));
    thus 0.ch = 0_(k,G);
    let A,B be Element of ch, A9,B9 be Chain of k,G;
    assume that
A5: A = A9 and
A6: B = B9;
    thus thesis by A1,A5,A6;
  end;
  uniqueness
  proof
    let C1,C2 be strict AbGroup;
    assume that
A7: the carrier of C1 = bool(cells(k,G)) and
A8: 0.C1 = 0_(k,G) and
A9: for A,B being Element of C1, A9,B9 being Chain of k,G st A = A9 &
    B = B9 holds A + B = A9 + B9 and
A10: the carrier of C2 = bool(cells(k,G)) and
A11: 0.C2 = 0_(k,G) and
A12: for A,B being Element of C2, A9,B9 being Chain of k,G st A = A9 &
    B = B9 holds A + B = A9 + B9;
    set X = [:bool(cells(k,G)),bool(cells(k,G)):];
    reconsider op1 = the addF of C1, op2 = the addF of C2 as
    Function of X,bool(cells(k,G)) by A7,A10;
    now
      let AB be Element of X;
      consider A9,B9 being Chain of k,G such that
A13:  AB = [A9,B9] by DOMAIN_1:1;
      reconsider A1 = A9, B1 = B9 as Element of C1 by A7;
      reconsider A2 = A9, B2 = B9 as Element of C2 by A10;
      thus op1.AB = A1 + B1 by A13
        .= A9 + B9 by A9
        .= A2 + B2 by A12
        .= op2.AB by A13;
    end;
    hence thesis by A7,A8,A10,A11,FUNCT_2:63;
  end;
end;

definition
  let d,G,k;
  mode GrChain of k,G is Element of Chains(k,G);
end;

theorem
  for x being set holds x is Chain of k,G iff x is GrChain of k,G by Def16;

definition
  let d,G,k;
  func del(k,G) -> Homomorphism of Chains(k + 1,G),Chains(k,G) means
  for A being Element of Chains(k + 1,G), A9 being Chain of (k + 1),G
  st A = A9 holds it.A = del A9;
  existence
  proof
    deffunc f(Subset of cells(k + 1,G)) = del $1;
    consider f being
    Function of bool(cells(k + 1,G)),bool(cells(k,G)) such that
    A1: for
 A being Subset of cells(k + 1,G) holds f.A = f(A) from FUNCT_2:sch 4;
A2: the carrier of Chains(k + 1,G) = bool(cells(k + 1,G)) by Def16;
    the carrier of Chains(k,G) = bool(cells(k,G)) by Def16;
    then reconsider f9 = f as Function of Chains(k + 1,G),Chains(k,G) by A2;
    now
      let A,B being Element of Chains(k + 1,G);
      reconsider A9 = A, B9 = B as Chain of (k + 1),G by Def16;
      thus f.(A + B) = f.(A9 + B9) by Def16
        .= del(A9 + B9) by A1
        .= del A9 + del B9 by Th61
        .= del A9 + f.B9 by A1
        .= f.A9 + f.B9 by A1
        .= f9.A + f9.B by Def16;
    end; then
    f9 is additive by VECTSP_1:def 20;
    then reconsider f9 as Homomorphism of Chains(k + 1,G),Chains(k,G);
    take f9;
    thus thesis by A1;
  end;
  uniqueness
  proof
    let f,g be Homomorphism of Chains(k + 1,G),Chains(k,G);
    assume
A3: for A being Element of Chains(k + 1,G), A9 being Chain of (k + 1),G
    st A = A9 holds f.A = del A9;
    assume
A4: for A being Element of Chains(k + 1,G), A9 being Chain of (k + 1),G
    st A = A9 holds g.A = del A9;
    now
      let A be Element of Chains(k + 1,G);
      reconsider A9 = A as Element of Chains(k + 1,G);
      reconsider A99 = A as Chain of (k + 1),G by Def16;
      f.A9 = del A99 by A3
        .= g.A9 by A4;
      hence f.A = g.A;
    end;
    hence f = g by FUNCT_2:63;
  end;
end;