chain_1.miz



    begin

    reserve X,x,y,z for set;

    reserve n,m,k,k9,d9 for Nat;

    theorem :: CHAIN_1:1

    

     Th1: for x,y be Real st x < y holds ex z be Element of REAL st x < z & z < y

    proof

      let x,y be Real;

      assume x < y;

      then

      consider z be Real such that

       A1: x < z and

       A2: z < y by XREAL_1: 5;

      reconsider z as Element of REAL by XREAL_0:def 1;

      take z;

      thus thesis by A1, A2;

    end;

    theorem :: CHAIN_1:2

    

     Th2: for x,y be Real holds ex z be Element of REAL st x < z & y < z

    proof

      let x,y be Real;

      reconsider x, y as Real;

      reconsider z = (( max (x,y)) + 1) as Element of REAL by XREAL_0:def 1;

      take z;

      

       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 :: CHAIN_1:sch1

    FrSet12 { D() -> non empty set , A() -> non empty set , P[ set, set], F( set, set) -> Element of D() } :

{ F(x,y) where x,y be Element of A() : P[x, y] } c= D();

      let z be object;

      assume z in { F(x,y) where x,y be Element of A() : P[x, y] };

      then ex x,y be Element of A() st z = F(x,y) & P[x, y];

      hence thesis;

    end;

    definition

      let B be set;

      let A be Subset of B;

      :: original: bool

      redefine

      func bool A -> Subset-Family of B ;

      coherence by ZFMISC_1: 67;

    end

    definition

      let d be real Element of NAT ;

      :: original: zero

      redefine

      :: CHAIN_1:def1

      attr d is zero means not d > 0 ;

      compatibility ;

    end

    definition

      let d be Nat;

      :: original: zero

      redefine

      :: CHAIN_1:def2

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

    reserve i,i0,i1 for Element of ( Seg d);

    theorem :: CHAIN_1:3

    

     Th3: for x,y be object holds {x, y} is trivial iff x = y

    proof

      let x,y be object;

      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;

      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 be object 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 be object 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 :: CHAIN_1:4

    

     Th4: X is trivial & (X \/ {y}) is non trivial implies ex x be object st X = {x}

    proof

      assume that

       A1: X is trivial and

       A2: (X \/ {y}) is non trivial;

      X is empty or ex x be object st X = {x} by A1, ZFMISC_1: 131;

      hence thesis by A2;

    end;

    scheme :: CHAIN_1:sch2

    NonEmptyFinite { X() -> non empty set , A() -> non empty finite Subset of X() , P[ set] } :

P[A()]

      provided

       A1: for x be Element of X() st x in A() holds P[ {x}]

       and

       A2: for x be Element of X(), B be non empty finite Subset of X() st x in A() & B c= A() & not x in B & P[B] holds P[(B \/ {x})];

      defpred Q[ set] means $1 is empty or P[$1];

      

       A3: A() is finite;

      

       A4: Q[ {} ];

      

       A5: for x,B be 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 :: CHAIN_1:sch3

    NonTrivialFinite { X() -> non trivial set , A() -> non trivial finite Subset of X() , P[ set] } :

P[A()]

      provided

       A1: for x,y be Element of X() st x in A() & y in A() & x <> y holds P[ {x, y}]

       and

       A2: for x be Element of X(), B be non trivial finite Subset of X() st x in A() & B c= A() & not x in B & P[B] holds P[(B \/ {x})];

      defpred Q[ set] means $1 is trivial or P[$1];

      

       A3: A() is finite;

      

       A4: Q[ {} ];

      

       A5: for x,B be 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 be object 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;

    theorem :: CHAIN_1:5

    

     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 be object such that

         A2: x <> y and

         A3: X9 = {x, y} by A1, CARD_2: 60;

        reconsider x, y as set by TARSKI: 1;

        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 be object 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;

    ::$Canceled

    theorem :: CHAIN_1:7

    

     Th6: for X,Y be 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 :: CHAIN_1:8

    

     Th7: for X,Y be 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, Th6;

      (( card (Y \ X)) is even iff ( card (X /\ Y)) is even) iff ( card Y) is even by A3, A4, Th6;

      hence thesis by A5, A6, A7, Th6;

    end;

    definition

      let n;

      :: original: REAL

      redefine

      :: CHAIN_1:def3

      func REAL n means

      : Def3: for x be object 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 be object holds x in X iff x is Function of ( Seg n), REAL by A1;

        assume

         A2: for x be object holds x in X iff x is Function of ( Seg n), REAL ;

        now

          let x be object;

          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: 2;

      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

    definition

      let d;

      :: CHAIN_1:def4

      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[ object, object] means $2 is non trivial finite Subset of REAL ;

        

         A1: for i be object st i in ( Seg d) holds ex X be object st P[i, X]

        proof

          let i be object;

          assume i in ( Seg d);

          set X = the non trivial finite Subset of REAL ;

          take X;

          thus thesis;

        end;

        consider G be Function such that

         A2: ( dom G) = ( Seg d) & for i be object st i in ( Seg d) holds P[i, (G . i)] from CLASSES1:sch 1( A1);

        for i be object st i in ( Seg d) holds (G . i) in ( bool REAL )

        proof

          let i be object;

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

        assume i in ( Seg d);

        hence (G . i) is finite by Def4;

      end;

    end

    definition

      let d, G, i;

      :: original: .

      redefine

      func G . i -> non trivial finite Subset of REAL ;

      coherence by Def4;

    end

    theorem :: CHAIN_1:9

    

     Th8: 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 be object st i in ( Seg d) holds (x . i) in (G . i);

      hence thesis by A1, A2, CARD_3: 9;

    end;

    ::$Canceled

    theorem :: CHAIN_1:11

    

     Th9: for X be non empty finite Subset of REAL holds ex ri be Element of REAL st ri in X & for xi st xi in X holds ri >= xi

    proof

      defpred P[ set] means ex ri be Element of REAL 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 be Element of REAL st xi in X holds P[ {xi}]

      proof

        let xi be Element of REAL ;

        assume xi in X;

        take xi;

        thus thesis by TARSKI:def 1;

      end;

      

       A2: for x be Element of REAL , B be 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 Element of 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;

          reconsider ri as Element of REAL by XREAL_0:def 1;

          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 :: CHAIN_1:12

    

     Th10: for X be non empty finite Subset of REAL holds ex li be Element of REAL st li in X & for xi st xi in X holds li <= xi

    proof

      defpred P[ set] means ex li be Element of REAL 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 be Element of REAL st xi in X holds P[ {xi}]

      proof

        let xi be Element of REAL ;

        assume xi in X;

        take xi;

        thus thesis by TARSKI:def 1;

      end;

      

       A2: for x be Element of REAL , B be 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 Element of 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;

          reconsider li as Element of REAL by XREAL_0:def 1;

          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 :: CHAIN_1:13

    

     Th11: 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 be Element of REAL ;

        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 be Element of REAL , B be 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 Element of 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;

    ::$Canceled

    theorem :: CHAIN_1:15

    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 be Element of REAL such that

       A1: li in Gi and

       A2: for xi st xi in Gi holds li >= xi by Th9;

      consider ri be Element of REAL such that

       A3: ri in Gi and

       A4: for xi st xi in Gi holds ri <= xi by Th10;

      take li, ri;

      

       A5: ri <= li by A2, A3;

      now

        assume

         A6: li = ri;

        consider x1,x2 be object such that

         A7: x1 in Gi and

         A8: x2 in Gi and

         A9: x1 <> x2 by ZFMISC_1:def 10;

        reconsider x1, x2 as Element of 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;

      :: CHAIN_1:def5

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

        reconsider ri, li as Element of REAL by XREAL_0:def 1;

        take [li, ri], li, ri;

        thus thesis by A1, A2, A3, A4;

      end;

    end

    theorem :: CHAIN_1:16

    

     Th13: [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;

      li in REAL & ri in REAL by XREAL_0:def 1;

      then [li, ri] in [: REAL , REAL :] by ZFMISC_1: 87;

      hence thesis by Def5;

    end;

    theorem :: CHAIN_1:17

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

        

         A4: ri9 in Gi by A2, Th13;

        

         A5: li9 = li or li9 = ri by A1, A3, TARSKI:def 2;

        li9 <> ri9 by A2, Th13;

        hence li9 = li & ri9 = ri or li9 = ri & ri9 = li by A1, A4, A5, TARSKI:def 2;

      end;

      assume

       A6: li9 = li & ri9 = ri or li9 = ri & ri9 = li;

      li9 in REAL & ri9 in REAL by XREAL_0:def 1;

      then [li9, ri9] in [: REAL , REAL :] by ZFMISC_1: 87;

      then

      reconsider liri = [li9, ri9] as Element of [: REAL , REAL :];

      liri is Gap of Gi

      proof

        take li9, ri9;

        li <> ri by A1, Th3;

        hence thesis by A1, TARSKI:def 2, XXREAL_0: 1, A6;

      end;

      hence thesis;

    end;

    deffunc f( set) = $1;

    theorem :: CHAIN_1:18

    

     Th15: xi in Gi implies ex ri be Element of REAL st [xi, ri] is Gap of Gi

    proof

      assume

       A1: xi in Gi;

      defpred P[ Element of REAL ] means $1 > xi;

      set Gi9 = { f(ri9) where ri9 be Element of REAL : 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 be Element of REAL such that

         A7: li in Gi and

         A8: for xi9 st xi9 in Gi holds li <= xi9 by Th10;

        take li;

         A9:

        now

          assume

           A10: li = xi;

          for xi9 be object holds xi9 in Gi iff xi9 = xi

          proof

            let xi9 be object;

            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, Th13;

      end;

        suppose Gi9 is non empty;

        then

        reconsider Gi9 as non empty finite Subset of REAL ;

        consider ri be Element of REAL such that

         A14: ri in Gi9 and

         A15: for ri9 st ri9 in Gi9 holds ri9 >= ri by Th10;

        take ri;

        now

          thus xi in Gi by A1;

          thus ri in Gi by A2, A14;

          ex ri9 be Element of REAL 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 Th13;

      end;

    end;

    theorem :: CHAIN_1:19

    

     Th16: xi in Gi implies ex li be Element of REAL st [li, xi] is Gap of Gi

    proof

      assume

       A1: xi in Gi;

      defpred P[ Element of REAL ] means $1 < xi;

      set Gi9 = { f(li9) where li9 be Element of REAL : 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 be Element of REAL such that

         A7: ri in Gi and

         A8: for xi9 st xi9 in Gi holds ri >= xi9 by Th9;

        take ri;

         A9:

        now

          assume

           A10: ri = xi;

          for xi9 be object holds xi9 in Gi iff xi9 = xi

          proof

            let xi9 be object;

            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, Th13;

      end;

        suppose Gi9 is non empty;

        then

        reconsider Gi9 as non empty finite Subset of REAL ;

        consider li be Element of REAL such that

         A14: li in Gi9 and

         A15: for li9 st li9 in Gi9 holds li9 <= li by Th9;

        take li;

        now

          thus xi in Gi by A1;

          thus li in Gi by A2, A14;

          ex li9 be Element of REAL 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 Th13;

      end;

    end;

    theorem :: CHAIN_1:20

    

     Th17: [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, Th13;

      

       A5: ri9 in Gi by A3, Th13;

      per cases by A2, Th13;

        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, Th13;

      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, Th13;

      end;

    end;

    theorem :: CHAIN_1:21

    

     Th18: [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, Th13;

      

       A5: li9 in Gi by A3, Th13;

      per cases by A2, Th13;

        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, Th13;

      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, Th13;

      end;

    end;

    theorem :: CHAIN_1:22

    

     Th19: 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, Th13;

      

       A6: ri in Gi by A2, Th13;

      

       A7: li9 in Gi by A4, Th13;

      

       A8: ri9 in Gi by A4, Th13;

      hereby

        assume li <> li9;

        then li < li9 or li9 < li by XXREAL_0: 1;

        hence contradiction by A1, A2, A3, A4, A5, A7, Th13;

      end;

      hereby

        assume ri <> ri9;

        then ri < ri9 or ri9 < ri by XXREAL_0: 1;

        hence contradiction by A1, A2, A3, A4, A6, A8, Th13;

      end;

    end;

    definition

      let d, l, r;

      :: CHAIN_1:def6

      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 :: CHAIN_1:23

    

     Th20: 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 :: CHAIN_1:24

    

     Th21: (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 Th20;

        hence for i holds (l . i) <= (x . i) & (x . i) <= (r . i) by A1;

      end;

      thus thesis;

    end;

    theorem :: CHAIN_1:25

    

     Th22: (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 Th20;

      thus thesis;

    end;

    theorem :: CHAIN_1:26

    

     Th23: 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 :: CHAIN_1:27

    

     Th24: ( cell (x,x)) = {x}

    proof

      for x9 be object holds x9 in ( cell (x,x)) iff x9 = x

      proof

        let x9 be object;

        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, Th21;

            (x9 . i) <= (x . i) by A1, A2, Th21;

            hence (x9 . i) = (x . i) by A3, XXREAL_0: 1;

          end;

          hence thesis by FUNCT_2: 63;

        end;

        thus thesis by Th23;

      end;

      hence thesis by TARSKI:def 1;

    end;

    theorem :: CHAIN_1:28

    

     Th25: (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), Element of REAL ] means $2 > (l . $1) & $2 > (r9 . $1);

          

           A4: for i holds ex xi be Element of REAL st P[i, xi] by Th2;

          consider x be 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, Th21;

        end;

          suppose

           A7: (l . i0) <= (r . i0);

          

           A8: l in ( cell (l,r)) by Th23;

          r in ( cell (l,r)) by Th23;

          hence thesis by A1, A2, A7, A8, Th21;

        end;

      end;

      assume

       A9: for i holds (l9 . i) <= (l . i) & (l . i) <= (r . i) & (r . i) <= (r9 . i);

      let x be object;

      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, Th21;

        

         A13: (x . i) <= (r . i) by A9, A10, Th21;

        (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 :: CHAIN_1:29

    

     Th26: (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), Element of 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 holds ex xi be Element of REAL 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 be Element of REAL st (r9 . i) < xi & xi < (l9 . i) by Th1;

              hence thesis by A6;

            end;

              suppose

               A7: (l9 . i) <= (r9 . i);

              ex xi be Element of REAL st (l . i) < xi & (r9 . i) < xi by Th2;

              hence thesis by A7;

            end;

          end;

          consider x be 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, Th20;

            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), Element of REAL ] means (r9 . $1) < $2 & $2 < (l9 . $1) & ($1 = i0 implies $2 < (r . $1));

          

           A12: for i holds ex xi be Element of REAL 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 be Element of REAL 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 be Element of REAL 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 be Element of REAL st ((r9 . i) < xi) & (xi < (l9 . i)) by Th1;

              hence thesis by A19;

            end;

          end;

          consider x be 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, Th20;

          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), Element of REAL ] means (l9 . $1) > $2 & $2 > (r9 . $1) & ($1 = i0 implies $2 > (l . $1));

          

           A24: for i holds ex xi be Element of REAL 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 be Element of REAL 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 be Element of REAL 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 be Element of REAL st ((r9 . i) < xi) & (xi < (l9 . i)) by Th1;

              hence thesis by A31;

            end;

          end;

          consider x be 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, Th20;

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

      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, Th20;

      

       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 :: CHAIN_1:30

    

     Th27: (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), Element of REAL ] means (l . $1) <= $2 & $2 <= (r . $1) & (r9 . $1) < $2 & $2 < (l9 . $1);

        

         A5: for i holds ex xi be Element of REAL 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 be Element of REAL 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);

            reconsider li = (l . i) as Element of REAL by XREAL_0:def 1;

            take li;

            thus thesis by A1, A4, A9;

          end;

            suppose

             A10: (r . i) < (l9 . i);

            reconsider ri = (r . i) as Element of REAL by XREAL_0:def 1;

            take ri;

            thus thesis by A1, A4, A10;

          end;

        end;

        consider x be 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, Th22;

        hence contradiction by A11;

      end;

      given i0 such that

       A13: (r . i0) <= (r9 . i0) or (l9 . i0) <= (l . i0);

      let x be object;

      assume

       A14: x in ( cell (l,r));

      then

      reconsider x as Element of ( REAL d);

      

       A15: (l . i0) <= (x . i0) by A1, A14, Th21;

      

       A16: (x . i0) <= (r . i0) by A1, A14, Th21;

      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 :: CHAIN_1:31

    

     Th28: (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, Th25;

          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, Th25;

            (l9 . i) <= (l . i) by A2, A4, Th25;

            hence (l . i) = (l9 . i) by A6, XXREAL_0: 1;

          end;

          now

            let i;

            

             A7: (r . i) <= (r9 . i) by A2, A4, Th25;

            (r9 . i) <= (r . i) by A2, A3, Th25;

            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, Th26;

          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, Th26;

            (l9 . i) <= (l . i) by A2, A8, Th26;

            hence (l . i) = (l9 . i) by A11, XXREAL_0: 1;

          end;

          now

            let i;

            

             A12: (r . i) <= (r9 . i) by A2, A8, Th26;

            (r9 . i) <= (r . i) by A2, A9, Th26;

            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;

      :: CHAIN_1:def7

      func cells (k,G) -> finite non empty Subset-Family of ( REAL d) equals

      : Def7: { ( cell (l,r)) : ((ex X be 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 be 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 be 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 Th11;

              reconsider li, ri as Element of REAL by XREAL_0:def 1;

              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 Element of REAL ;

              reconsider lri = [li, li] as Element of [: REAL , REAL :];

              take lri;

              thus thesis by A8;

            end;

          end;

        end;

        consider lr be 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 be 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 be 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 be 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[ object, Element of ( REAL d), Element of ( REAL d), object] 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[ object, object] means ex l, r st Q[$1, l, r, $2];

        

         A24: for A be object st A in CELLS holds ex lr be object st S[A, lr]

        proof

          let A be object;

          assume A in CELLS;

          then

          consider l, r such that

           A25: A = ( cell (l,r)) and

           A26: (ex X be 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 be 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 Th13;

            end;

            hence l in ( product G) & r in ( product G) by Th8;

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

            end;

            hence l in ( product G) & r in ( product G) by Th8;

            thus thesis by A25;

          end;

        end;

        consider f be Function such that

         A29: ( dom f) = CELLS & for A be object 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 object;

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

          assume lr in ( rng f);

          then

          consider A be object 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 :: CHAIN_1:32

    

     Th29: k <= d implies for A be Subset of ( REAL d) holds A in ( cells (k,G)) iff ex l, r st A = ( cell (l,r)) & ((ex X be 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 be 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 :: CHAIN_1:33

    

     Th30: k <= d implies (( cell (l,r)) in ( cells (k,G)) iff ((ex X be 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 be 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, Th29;

        l = l9 & r = r9

        proof

          per cases by A3;

            suppose ex X be 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, Th28;

          end;

            suppose for i holds (r9 . i) < (l9 . i) & [(l9 . i), (r9 . i)] is Gap of (G . i);

            hence thesis by A2, Th28;

          end;

        end;

        hence (ex X be 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, Th29;

    end;

    theorem :: CHAIN_1:34

    

     Th31: 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, Th30;

        suppose ex X be 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 :: CHAIN_1:35

    

     Th32: 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, Th31;

      hence thesis by Th13;

    end;

    theorem :: CHAIN_1:36

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

    theorem :: CHAIN_1:37

    

     Th34: for A be 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 be 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 Th29;

        consider X be 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 be 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, Th29;

    end;

    theorem :: CHAIN_1:38

    

     Th35: ( 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 Th34;

        

         A3: for i holds (x . i) <= (x . i);

        then l = x by A1, Th28;

        hence l = r & for i holds (l . i) in (G . i) by A1, A2, A3, Th28;

      end;

      thus thesis by Th34;

    end;

    theorem :: CHAIN_1:39

    

     Th36: for A be 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 be 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 Th29;

        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 be 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 be 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 be 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, Th29;

      end;

        suppose for i holds (r . i) < (l . i);

        hence thesis by A5, A6, Th29;

      end;

    end;

    theorem :: CHAIN_1:40

    

     Th37: ( 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 Th36;

        

         A4: (for i holds (l9 . i) <= (r9 . i)) or for i holds (r9 . i) < (l9 . i) by A3;

        then

         A5: l = l9 by A1, Th28;

        r = r9 by A1, A4, Th28;

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

    end;

    theorem :: CHAIN_1:41

    

     Th38: d = (d9 + 1) implies for A be 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 be 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, Th29;

        take l, r;

        consider X be 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 be object 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, Th29;

    end;

    theorem :: CHAIN_1:42

    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, Th38;

        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, Th28;

        r = r9 by A2, A6, Th28;

        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, Th38;

    end;

    theorem :: CHAIN_1:43

    

     Th40: for A be 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 be 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, Th29;

        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 be 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 be 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 be object 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, Th29;

      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, Th29;

      end;

    end;

    theorem :: CHAIN_1:44

    ( 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 Th40;

        

         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, Th28;

        r = r9 by A1, A5, Th28;

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

    end;

    theorem :: CHAIN_1:45

    

     Th42: 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, Th31;

        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, Th25;

        

         A9: (l . i) <= (r . i) by A5, A7, Th25;

        

         A10: (r . i) <= (r9 . i) by A5, A7, Th25;

        

         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, Th32;

              hence contradiction by A13, A17, A18, Th13;

            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, Th32;

              hence contradiction by A13, A21, A22, Th13;

            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, Th31;

            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, Th26;

            

             A28: (l9 . i) <= (l . i) by A5, A26, Th26;

             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, Th32;

              hence contradiction by A24, A25, A30, Th13;

            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, Th32;

              hence contradiction by A24, A25, A31, Th13;

            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, Th32;

            (r . i) in (G . i) by A1, A3, Th32;

            hence thesis by A24, A25, A32, A33, Th13;

          end;

        end;

      end;

    end;

    theorem :: CHAIN_1:46

    

     Th43: 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 be 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, Th30;

      

       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 be object 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, Th42;

        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), Element of REAL ] means (l . $1) <= $2 & $2 <= (r . $1) & (r9 . $1) < $2 & $2 < (l9 . $1);

        

         A14: for i holds ex xi be Element of REAL st P[i, xi]

        proof

          let i;

          

           A15: (l . i) in (G . i) by A3, A5, Th32;

          

           A16: (r . i) in (G . i) by A3, A5, Th32;

          

           A17: (r9 . i) < (l9 . i) by A2, A4, A12, Th31;

          

           A18: [(l9 . i), (r9 . i)] is Gap of (G . i) by A2, A4, A12, Th31;

          per cases ;

            suppose

             A19: (r9 . i) < (l . i) & (l . i) < (l9 . i);

            reconsider li = (l . i) as Element of REAL by XREAL_0:def 1;

            take li;

            thus thesis by A8, A19;

          end;

            suppose

             A20: (l . i) <= (r9 . i);

            

             A21: (l . i) >= (r9 . i) by A15, A17, A18, Th13;

            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 be Element of REAL such that

             A23: (l . i) < xi and

             A24: xi < (r . i) by Th1;

            take xi;

            (r . i) <= (l9 . i) by A16, A17, A18, Th13;

            hence thesis by A21, A23, A24, XXREAL_0: 2;

          end;

            suppose

             A25: (l9 . i) <= (l . i);

            (l9 . i) >= (l . i) by A15, A17, A18, Th13;

            then

             A26: (l9 . i) = (l . i) by A25, XXREAL_0: 1;

            (l9 . i) >= (r . i) by A16, A17, A18, Th13;

            then (l9 . i) = (r . i) by A8, A26;

            hence thesis by A13, A26;

          end;

        end;

        consider x be 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, Th22;

      end;

    end;

    theorem :: CHAIN_1:47

    

     Th44: for X,X9 be 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 Th23;

      

       A5: r in ( cell (l,r)) by Th23;

      

       A6: for i holds (l9 . i) <= (r9 . i) by A3;

      thus X c= X9

      proof

        let i be object;

        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, Th21;

        (r . i) <= (r9 . i) by A1, A5, A6, Th21;

        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, Th30;

      

       A16: ( cell (l9,r9)) in ( cells (k9,G)) by A3, A14, Th30;

      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, Th42;

        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, Th42;

      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;

      :: CHAIN_1:def8

      func 0_ (k,G) -> Chain of k, G equals {} ;

      coherence by SUBSET_1: 1;

    end

    definition

      let d, G;

      :: CHAIN_1:def9

      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;

      :: original: +

      redefine

      func C1 + C2 -> Chain of k, G ;

      coherence

      proof

        (C1 \+\ C2) c= ( cells (k,G));

        hence thesis;

      end;

    end

    definition

      let d, G;

      :: CHAIN_1:def10

      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), Element of REAL ] means $2 in (G . $1) & for xi st xi in (G . $1) holds xi <= $2;

        

         A1: for i holds ex li be Element of REAL st P[i, li] by Th9;

        consider l be 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), Element of REAL ] means $2 in (G . $1) & for xi st xi in (G . $1) holds xi >= $2;

        

         A3: for i holds ex ri be Element of REAL st R[i, ri] by Th10;

        consider r be 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 object 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 Element of 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, Th13;

        end;

        then

        reconsider A = ( cell (l,r)) as Cell of d, G by Th30;

        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, Th19;

        end;

        then l = l9 by FUNCT_2: 63;

        hence thesis by A19, A21, A23, FUNCT_2: 63;

      end;

    end

    theorem :: CHAIN_1:48

    

     Th45: ( 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, Th28;

        r = r9 by A2, A3, Th28;

        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, Th31;

      hence thesis by A6, Def10;

    end;

    theorem :: CHAIN_1:49

    

     Th46: ( 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, Th28;

        r = r9 by A1, A2, Th28;

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

      hence thesis by A4, Def10;

    end;

    scheme :: CHAIN_1:sch4

    ChainInd { d() -> non zero Nat , G() -> Grating of d() , k() -> Nat , C() -> Chain of k(), G() , P[ set] } :

P[C()]

      provided

       A1: P[( 0_ (k(),G()))]

       and

       A2: for A be Cell of k(), G() st A in C() holds P[ {A}]

       and

       A3: for C1,C2 be Chain of k(), G() st C1 c= C() & C2 c= C() & P[C1] & P[C2] holds P[(C1 + C2)];

      

       A4: C() is finite;

      

       A5: P[ {} ] by A1;

      

       A6: for x,B be 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 object;

            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;

    definition

      let d, G, k;

      let A be Cell of k, G;

      :: CHAIN_1:def11

      func star A -> Chain of (k + 1), G equals { B where B be Cell of (k + 1), G : A c= B };

      coherence

      proof

        defpred P[ set] means A c= $1;

        { B where B be Cell of (k + 1), G : P[B] } c= ( cells ((k + 1),G)) from FRAENKEL:sch 10;

        hence thesis;

      end;

    end

    theorem :: CHAIN_1:50

    

     Th47: for A be Cell of k, G, B be 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 be 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;

      :: CHAIN_1:def12

      func del C -> Chain of k, G equals { A where A be 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 be 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;

      :: CHAIN_1:def13

      pred C9 bounds C means C9 = ( del C);

    end

    theorem :: CHAIN_1:51

    

     Th48: for A be Cell of k, G, C be 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 be Cell of k, G : P[A9] };

      thus A in ( del C) iff P[A] from LMOD_7:sch 7( A1);

    end;

    theorem :: CHAIN_1:52

    

     Th49: (k + 1) > d implies for C be 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 be object holds not A in ( del C) by A1, Th48;

      hence thesis by XBOOLE_0:def 1;

    end;

    theorem :: CHAIN_1:53

    

     Th50: (k + 1) <= d implies for A be Cell of k, G, B be 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 object;

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

            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, Th47, Th48;

    end;

    theorem :: CHAIN_1:54

    

     Th51: d = (d9 + 1) implies for A be 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, Th38;

       A7:

      now

        let i;

        i = i0 or i <> i0;

        hence (l . i) <= (r . i) by A4, A6;

      end;

      ex B1,B2 be set st B1 in ( star A) & B2 in ( star A) & B1 <> B2 & for B be 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 be Element of REAL such that

           A8: [l1i0, (l . i0)] is Gap of (G . i0) by A5, Th16;

          per cases by A8, Th13;

            suppose

             A9: l1i0 < (l . i0);

            defpred P[ Element of ( Seg d), Element of REAL ] means ($1 = i0 implies $2 = l1i0) & ($1 <> i0 implies $2 = (l . $1));

            

             A10: for i holds ex li be Element of REAL st P[i, li]

            proof

              let i;

              

               A11: (l . i) in REAL by XREAL_0:def 1;

              i = i0 or i <> i0;

              hence thesis by A11;

            end;

            consider l1 be Function of ( Seg d), REAL such that

             A12: 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, A12;

          end;

            suppose

             A13: (l . i0) < l1i0;

            consider l1, r1 such that ( cell (l1,r1)) = ( infinite-cell G) and

             A14: for i holds (r1 . i) < (l1 . i) & [(l1 . i), (r1 . i)] is Gap of (G . i) by Def10;

            take l1, r1;

            

             A15: (r1 . i0) < (l1 . i0) by A14;

             [(l1 . i0), (r1 . i0)] is Gap of (G . i0) by A14;

            hence thesis by A8, A13, A14, A15, Th19;

          end;

        end;

        then

        consider l1, r1 such that

         A16: [(l1 . i0), (r1 . i0)] is Gap of (G . i0) and

         A17: (r1 . i0) = (l . i0) and

         A18: ((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);

         A19:

        now

          let i;

          

           A20: 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 A16, A18, A20;

        end;

        

         A21: (for i holds (l1 . i) < (r1 . i)) or for i holds (r1 . i) < (l1 . i)

        proof

          per cases by A18;

            suppose

             A22: (l1 . i0) < (r1 . i0) & for i st i <> i0 holds (l1 . i) = (l . i) & (r1 . i) = (r . i);

            now

              let i;

              

               A23: 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 A22, A23;

            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 A19, Th37;

        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 be Element of REAL such that

           A24: [(l . i0), r2i0] is Gap of (G . i0) by A5, Th15;

          per cases by A24, Th13;

            suppose

             A25: (l . i0) < r2i0;

            defpred P[ Element of ( Seg d), Element of REAL ] means ($1 = i0 implies $2 = r2i0) & ($1 <> i0 implies $2 = (r . $1));

            

             A26: for i holds ex ri be Element of REAL st P[i, ri]

            proof

              let i;

              

               A27: (r . i) in REAL by XREAL_0:def 1;

              i = i0 or i <> i0;

              hence thesis by A27;

            end;

            consider r2 be Function of ( Seg d), REAL such that

             A28: for i holds P[i, (r2 . i)] from FUNCT_2:sch 3( A26);

            reconsider r2 as Element of ( REAL d) by Def3;

            take l, r2;

            thus thesis by A24, A25, A28;

          end;

            suppose

             A29: r2i0 < (l . i0);

            consider l2, r2 such that ( cell (l2,r2)) = ( infinite-cell G) and

             A30: for i holds (r2 . i) < (l2 . i) & [(l2 . i), (r2 . i)] is Gap of (G . i) by Def10;

            take l2, r2;

            

             A31: (r2 . i0) < (l2 . i0) by A30;

             [(l2 . i0), (r2 . i0)] is Gap of (G . i0) by A30;

            hence thesis by A24, A29, A30, A31, Th19;

          end;

        end;

        then

        consider l2, r2 such that

         A32: [(l2 . i0), (r2 . i0)] is Gap of (G . i0) and

         A33: (l2 . i0) = (l . i0) and

         A34: ((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);

         A35:

        now

          let i;

          

           A36: 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 A32, A34, A36;

        end;

        (for i holds (l2 . i) < (r2 . i)) or for i holds (r2 . i) < (l2 . i)

        proof

          per cases by A34;

            suppose

             A37: (l2 . i0) < (r2 . i0) & for i st i <> i0 holds (l2 . i) = (l . i) & (r2 . i) = (r . i);

            now

              let i;

              

               A38: 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 A37, A38;

            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 A35, Th37;

        take B1, B2;

        A c= B1

        proof

          per cases by A18;

            suppose

             A39: (l1 . i0) < (r1 . i0) & for i st i <> i0 holds (l1 . i) = (l . i) & (r1 . i) = (r . i);

             A40:

            now

              let i;

              i = i0 or i <> i0 & (l1 . i) = (l . i) & (r1 . i) = (r . i) by A39;

              hence (l1 . i) <= (r1 . i) by A6, A39;

            end;

            now

              let i;

              i = i0 or i <> i0 & (l1 . i) = (l . i) & (r1 . i) = (r . i) by A39;

              hence (l1 . i) <= (l . i) & (l . i) <= (r . i) & (r . i) <= (r1 . i) by A4, A17, A40;

            end;

            hence thesis by A3, A40, Th25;

          end;

            suppose for i holds (r1 . i) < (l1 . i) & [(l1 . i), (r1 . i)] is Gap of (G . i);

            hence thesis by A3, A4, A7, A17, Th27;

          end;

        end;

        hence B1 in ( star A) by A1;

        A c= B2

        proof

          per cases by A34;

            suppose

             A41: (l2 . i0) < (r2 . i0) & for i st i <> i0 holds (l2 . i) = (l . i) & (r2 . i) = (r . i);

             A42:

            now

              let i;

              i = i0 or i <> i0 & (l2 . i) = (l . i) & (r2 . i) = (r . i) by A41;

              hence (l2 . i) <= (r2 . i) by A6, A41;

            end;

            now

              let i;

              i = i0 or i <> i0 & (l2 . i) = (l . i) & (r2 . i) = (r . i) by A41;

              hence (l2 . i) <= (l . i) & (l . i) <= (r . i) & (r . i) <= (r2 . i) by A4, A33, A42;

            end;

            hence thesis by A3, A42, Th25;

          end;

            suppose for i holds (r2 . i) < (l2 . i) & [(l2 . i), (r2 . i)] is Gap of (G . i);

            hence thesis by A3, A7, A33, Th27;

          end;

        end;

        hence B2 in ( star A) by A1;

        

         A43: l1 <> l2 by A17, A18, A33;

        (for i holds (l1 . i) <= (r1 . i)) or for i holds (r1 . i) < (l1 . i) by A21;

        hence B1 <> B2 by A43, Th28;

        let B be set;

        assume

         A44: B in ( star A);

        then

        reconsider B as Cell of d, G by A1;

        consider l9, r9 such that

         A45: B = ( cell (l9,r9)) and

         A46: for i holds [(l9 . i), (r9 . i)] is Gap of (G . i) and

         A47: (for i holds (l9 . i) < (r9 . i)) or for i holds (r9 . i) < (l9 . i) by Th36;

        

         A48: [(l9 . i0), (r9 . i0)] is Gap of (G . i0) by A46;

        

         A49: A c= B by A44, Th47;

        per cases by A47;

          suppose

           A50: for i holds (l9 . i) < (r9 . i);

           A51:

          now

            let i;

            assume

             A52: i <> i0;

            (l9 . i) < (r9 . i) by A50;

            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, A45, A49, Th42;

            hence (l9 . i) = (l . i) & (r9 . i) = (r . i) by A6, A52;

          end;

          thus thesis

          proof

            

             A53: (l9 . i0) < (r9 . i0) by A50;

            per cases by A2, A3, A4, A45, A49, A53, Th42;

              suppose

               A54: (l . i0) = (r9 . i0) & (r . i0) = (r9 . i0);

              then

               A55: (l9 . i0) = (l1 . i0) by A16, A17, A48, Th18;

              reconsider l9, r9, l1, r1 as Function of ( Seg d), REAL by Def3;

               A56:

              now

                let i;

                

                 A57: (l1 . i0) < (l . i0) by A50, A54, A55;

                then i = i0 or i <> i0 & (l9 . i) = (l . i) & (l1 . i) = (l . i) by A17, A18, A51;

                hence (l9 . i) = (l1 . i) by A16, A17, A48, A54, Th18;

                i = i0 or i <> i0 & (r9 . i) = (r . i) & (r1 . i) = (r . i) by A17, A18, A51, A57;

                hence (r9 . i) = (r1 . i) by A17, A54;

              end;

              then l9 = l1 by FUNCT_2: 63;

              hence thesis by A45, A56, FUNCT_2: 63;

            end;

              suppose

               A58: (l . i0) = (l9 . i0) & (r . i0) = (l9 . i0);

              then

               A59: (r9 . i0) = (r2 . i0) by A32, A33, A48, Th17;

              reconsider l9, r9, l2, r2 as Function of ( Seg d), REAL by Def3;

               A60:

              now

                let i;

                

                 A61: (l . i0) < (r2 . i0) by A50, A58, A59;

                then i = i0 or i <> i0 & (r9 . i) = (r . i) & (r2 . i) = (r . i) by A33, A34, A51;

                hence (r9 . i) = (r2 . i) by A32, A33, A48, A58, Th17;

                i = i0 or i <> i0 & (l9 . i) = (l . i) & (l2 . i) = (l . i) by A33, A34, A51, A61;

                hence (l9 . i) = (l2 . i) by A33, A58;

              end;

              then l9 = l2 by FUNCT_2: 63;

              hence thesis by A45, A60, FUNCT_2: 63;

            end;

          end;

        end;

          suppose

           A62: for i holds (r9 . i) < (l9 . i);

          consider i1 such that

           A63: (l . i1) = (l9 . i1) & (r . i1) = (l9 . i1) or (l . i1) = (r9 . i1) & (r . i1) = (r9 . i1) by A2, A3, A45, A49, Th43;

          

           A64: i0 = i1 by A6, A63;

          thus thesis

          proof

            per cases by A63, A64;

              suppose

               A65: (l . i0) = (r9 . i0) & (r . i0) = (r9 . i0);

              then (l9 . i0) = (l1 . i0) by A16, A17, A48, Th18;

              then B1 = ( infinite-cell G) by A17, A18, A62, A65, Th45;

              hence thesis by A45, A62, Th45;

            end;

              suppose

               A66: (l . i0) = (l9 . i0) & (r . i0) = (l9 . i0);

              then (r9 . i0) = (r2 . i0) by A32, A33, A48, Th17;

              then B2 = ( infinite-cell G) by A33, A34, A62, A66, Th45;

              hence thesis by A45, A62, Th45;

            end;

          end;

        end;

      end;

      hence thesis by Th5;

    end;

    theorem :: CHAIN_1:55

    

     Th52: for G be Grating of d, B be 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 Th40;

      ex A1,A2 be set st A1 in ( del {B}) & A2 in ( del {B}) & A1 <> A2 & for A be 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, Th32;

        then

        reconsider A1 = ( cell (l,l)), A2 = ( cell (r,r)) as Cell of 0 , G by Th35;

        take A1, A2;

        

         A6: A1 = {l} by Th24;

        

         A7: A2 = {r} by Th24;

        

         A8: l in B by A2, Th23;

        

         A9: r in B by A2, Th23;

        

         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, Th50;

        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, Th50;

        consider x such that

         A13: A = ( cell (x,x)) and

         A14: for i holds (x . i) in (G . i) by Th34;

        

         A15: x in A by A13, Th23;

        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, Th21;

          

           A20: (x . i0) <= (r . i0) by A2, A12, A15, A17, Th21;

          

           A21: not ((l . i0) < (x . i0) & (x . i0) < (r . i0)) by A4, A18, Th13;

           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, Th21;

            (x . i) <= (r . i) by A2, A12, A15, A17, Th21;

            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, Th22;

          

           A34: i1 = i0 by A28;

          

           A35: (x . i0) in (G . i0) by A14;

          then

           A36: not (x . i0) < (r . i0) by A4, A27, Th13;

          

           A37: not (l . i0) < (x . i0) by A4, A27, A35, Th13;

          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;

    theorem :: CHAIN_1:56

    ( Omega G) = (( 0_ (d,G)) ` ) & ( 0_ (d,G)) = (( Omega G) ` )

    proof

      ( Omega G) = (( 0_ (d,G)) ` );

      hence thesis;

    end;

    theorem :: CHAIN_1:57

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

    theorem :: CHAIN_1:58

    

     Th55: for C be 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 :: CHAIN_1:59

    

     Th56: ( 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 Th48;

      end;

      hence thesis by SUBSET_1: 3;

    end;

    theorem :: CHAIN_1:60

    

     Th57: for G be 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 Th51;

        hence A in ( del ( Omega G)) iff A in ( 0_ (d9,G)) by Th48;

      end;

      hence thesis by SUBSET_1: 3;

    end;

    theorem :: CHAIN_1:61

    

     Th58: for C1,C2 be 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 Th48;

        

         A3: A in ( del C1) iff (k + 1) <= d & ( card (( star A) /\ C1)) is odd by Th48;

        A in ( del C2) iff (k + 1) <= d & ( card (( star A) /\ C2)) is odd by Th48;

        hence A in ( del (C1 + C2)) iff A in (( del C1) + ( del C2)) by A1, A2, A3, Th7, XBOOLE_0: 1;

      end;

      hence thesis by SUBSET_1: 3;

    end;

    theorem :: CHAIN_1:62

    

     Th59: for G be Grating of (d9 + 1), C be 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 Th55

      .= (( del C) + ( del ( Omega G))) by Th58

      .= (( del C) + ( 0_ (d9,G))) by Th57

      .= ( del C);

    end;

    theorem :: CHAIN_1:63

    

     Th60: for C be 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 be 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 object;

            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, Th47, Th50;

            end;

            

             A9: ( card BB) is odd by A7, Th48;

            consider B be object 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;

            set i0 = the Element of ( Seg d);

            (l . i0) <= (r . i0) by A6;

            then

            consider Z be 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, Th30;

            consider l9, r9 such that

             A15: A = ( cell (l9,r9)) and

             A16: (ex X be 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, Th29;

            (l9 . i0) <= (r9 . i0) by A5, A6, A12, A15, Th25;

            then

            consider X be 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 be set st B1 in BB & B2 in BB & B1 <> B2 & for B be set st B in BB holds B = B1 or B = B2

            proof

              

               A19: X c= Z by A5, A12, A14, A15, A18, Th44;

              

              then ( card (Z \ X)) = ((k + (1 + 1)) - k) by A13, A17, CARD_2: 44

              .= 2;

              then

              consider i1,i2 be set such that

               A20: i1 in (Z \ X) and

               A21: i2 in (Z \ X) and

               A22: i1 <> i2 and

               A23: for i be 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), Element of REAL ] means ($1 in Y1 implies $2 = (l . $1)) & ( not $1 in Y1 implies $2 = (l9 . $1));

              

               A30: for i holds ex xi be Element of REAL st S[i, xi]

              proof

                let i;

                

                 A31: (l . i) in REAL & (l9 . i) in REAL by XREAL_0:def 1;

                i in Y1 or not i in Y1;

                hence thesis by A31;

              end;

              consider l1 be Function of ( Seg d), REAL such that

               A32: for i holds S[i, (l1 . i)] from FUNCT_2:sch 3( A30);

              defpred R[ Element of ( Seg d), Element of REAL ] means ($1 in Y1 implies $2 = (r . $1)) & ( not $1 in Y1 implies $2 = (r9 . $1));

              

               A33: for i holds ex xi be Element of REAL st R[i, xi]

              proof

                let i;

                

                 A34: (r . i) in REAL & (r9 . i) in REAL by XREAL_0:def 1;

                i in Y1 or not i in Y1;

                hence thesis by A34;

              end;

              consider r1 be Function of ( Seg d), REAL such that

               A35: for i holds R[i, (r1 . i)] from FUNCT_2:sch 3( A33);

              reconsider l1, r1 as Element of ( REAL d) by Def3;

              

               A36: 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 A32, A35;

                hence thesis by A14, A18;

              end;

              

               A37: ( 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

                   A38: i in Y1;

                  then

                   A39: (l1 . i) = (l . i) by A32;

                  (r1 . i) = (r . i) by A35, A38;

                  hence thesis by A14, A29, A38, A39;

                end;

                  suppose

                   A40: not i in Y1;

                  then

                   A41: (l1 . i) = (l9 . i) by A32;

                  

                   A42: (r1 . i) = (r9 . i) by A35, A40;

                   not i in X by A28, A40;

                  hence thesis by A18, A40, A41, A42;

                end;

              end;

              then

              reconsider B1 = ( cell (l1,r1)) as Cell of (k + 1), G by A2, A37, Th30;

              set Y2 = (X \/ {i2});

              

               A43: X c= Y2 by XBOOLE_1: 7;

               {i2} c= Z by A25, ZFMISC_1: 31;

              then

               A44: Y2 c= Z by A19, XBOOLE_1: 8;

              defpred P[ Element of ( Seg d), Element of REAL ] means ($1 in Y2 implies $2 = (l . $1)) & ( not $1 in Y2 implies $2 = (l9 . $1));

              

               A45: for i holds ex xi be Element of REAL st P[i, xi]

              proof

                let i;

                

                 A46: (l . i) in REAL & (l9 . i) in REAL by XREAL_0:def 1;

                i in Y2 or not i in Y2;

                hence thesis by A46;

              end;

              consider l2 be Function of ( Seg d), REAL such that

               A47: for i holds P[i, (l2 . i)] from FUNCT_2:sch 3( A45);

              defpred R[ Element of ( Seg d), Element of REAL ] means ($1 in Y2 implies $2 = (r . $1)) & ( not $1 in Y2 implies $2 = (r9 . $1));

              

               A48: for i holds ex xi be Element of REAL st R[i, xi]

              proof

                let i;

                

                 A49: (r . i) in REAL & (r9 . i) in REAL by XREAL_0:def 1;

                i in Y2 or not i in Y2;

                hence thesis by A49;

              end;

              consider r2 be Function of ( Seg d), REAL such that

               A50: for i holds R[i, (r2 . i)] from FUNCT_2:sch 3( A48);

              reconsider l2, r2 as Element of ( REAL d) by Def3;

              

               A51: ( 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

                   A52: i in Y2;

                  then

                   A53: (l2 . i) = (l . i) by A47;

                  (r2 . i) = (r . i) by A50, A52;

                  hence thesis by A14, A44, A52, A53;

                end;

                  suppose

                   A54: not i in Y2;

                  then

                   A55: (l2 . i) = (l9 . i) by A47;

                  

                   A56: (r2 . i) = (r9 . i) by A50, A54;

                   not i in X by A43, A54;

                  hence thesis by A18, A54, A55, A56;

                end;

              end;

              then

              reconsider B2 = ( cell (l2,r2)) as Cell of (k + 1), G by A2, A51, Th30;

              take B1, B2;

              

               A57: 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

                   A58: i in Y1;

                  then

                   A59: (l1 . i) = (l . i) by A32;

                  (r1 . i) = (r . i) by A35, A58;

                  hence thesis by A5, A6, A12, A15, A59, Th25;

                end;

                  suppose

                   A60: not i in Y1;

                  then

                   A61: (l1 . i) = (l9 . i) by A32;

                  (r1 . i) = (r9 . i) by A35, A60;

                  hence thesis by A5, A6, A12, A15, A61, Th25;

                end;

              end;

              then

               A62: A c= B1 by A15, Th25;

              B1 c= C by A5, A6, A57, Th25;

              hence B1 in BB by A8, A62;

              

               A63: 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

                   A64: i in Y2;

                  then

                   A65: (l2 . i) = (l . i) by A47;

                  (r2 . i) = (r . i) by A50, A64;

                  hence thesis by A5, A6, A12, A15, A65, Th25;

                end;

                  suppose

                   A66: not i in Y2;

                  then

                   A67: (l2 . i) = (l9 . i) by A47;

                  (r2 . i) = (r9 . i) by A50, A66;

                  hence thesis by A5, A6, A12, A15, A67, Th25;

                end;

              end;

              then

               A68: A c= B2 by A15, Th25;

              B2 c= C by A5, A6, A63, Th25;

              hence B2 in BB by A8, A68;

              i1 in {i1} by TARSKI:def 1;

              then

               A69: i1 in Y1 by XBOOLE_0:def 3;

              

               A70: not i1 in X by A20, XBOOLE_0:def 5;

               not i1 in {i2} by A22, TARSKI:def 1;

              then

               A71: not i1 in Y2 by A70, XBOOLE_0:def 3;

              

               A72: (l1 . i1) = (l . i1) by A32, A69;

              

               A73: (r1 . i1) = (r . i1) by A35, A69;

              

               A74: (l2 . i1) = (l9 . i1) by A47, A71;

              

               A75: (r2 . i1) = (r9 . i1) by A50, A71;

              (l . i1) < (r . i1) by A14, A24;

              then l1 <> l2 or r1 <> r2 by A18, A26, A72, A73, A74, A75;

              hence B1 <> B2 by A36, Th28;

              let B be set;

              assume

               A76: B in BB;

              then

              reconsider B as Cell of (k + 1), G;

              

               A77: A c= B by A8, A76;

              

               A78: B c= C by A8, A76;

              consider l99, r99 such that

               A79: B = ( cell (l99,r99)) and

               A80: (ex Y be 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, Th29;

              (l99 . i0) <= (r99 . i0) by A5, A6, A78, A79, Th25;

              then

              consider Y be Subset of ( Seg d) such that

               A81: ( card Y) = (k + 1) and

               A82: 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 A80;

              

               A83: X c= Y by A15, A18, A77, A79, A82, Th44;

              

               A84: Y c= Z by A5, A14, A78, A79, A82, Th44;

              ( card (Y \ X)) = ((k + 1) - k) by A17, A81, A83, CARD_2: 44

              .= 1;

              then

              consider i9 be object such that

               A85: (Y \ X) = {i9} by CARD_2: 42;

              

               A86: i9 in (Y \ X) by A85, TARSKI:def 1;

              then

              reconsider i9 as Element of ( Seg d);

              

               A87: i9 in Y by A86, XBOOLE_0:def 5;

               not i9 in X by A86, XBOOLE_0:def 5;

              then

               A88: i9 in (Z \ X) by A84, A87, XBOOLE_0:def 5;

              

               A89: Y = (X \/ Y) by A83, XBOOLE_1: 12

              .= (X \/ {i9}) by A85, XBOOLE_1: 39;

              per cases by A23, A88, A89;

                suppose

                 A90: Y = Y1;

                reconsider l99, r99, l1, r1 as Function of ( Seg d), REAL by Def3;

                 A91:

                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, A32, A35, A77, A78, A79, A82, A90, Th44;

                  hence (l99 . i) = (l1 . i) & (r99 . i) = (r1 . i);

                end;

                then l99 = l1 by FUNCT_2: 63;

                hence thesis by A79, A91, FUNCT_2: 63;

              end;

                suppose

                 A92: Y = Y2;

                reconsider l99, r99, l2, r2 as Function of ( Seg d), REAL by Def3;

                 A93:

                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, A47, A50, A77, A78, A79, A82, A92, Th44;

                  hence (l99 . i) = (l2 . i) & (r99 . i) = (r2 . i);

                end;

                then l99 = l2 by FUNCT_2: 63;

                hence thesis by A79, A93, FUNCT_2: 63;

              end;

            end;

            then ( card BB) = (2 * 1) by Th5;

            hence contradiction by A7, Th48;

          end;

          hence thesis by XBOOLE_0:def 1;

        end;

        

         A94: for C1,C2 be 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

           A95: ( del ( del C1)) = ( 0_ (k,G)) and

           A96: ( del ( del C2)) = ( 0_ (k,G));

          

          thus ( del ( del (C1 + C2))) = ( del (( del C1) + ( del C2))) by Th58

          .= (( 0_ (k,G)) + ( 0_ (k,G))) by A95, A96, Th58

          .= ( 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 Th56

        .= ( 0_ (k,G)) by Th56;

        then

         A97: P[( 0_ (((k + 1) + 1),G))];

        for A be 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

           A98: A = ( cell (l,r)) and

           A99: (ex X be 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, Th29;

          per cases by A99;

            suppose ex X be 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, A98;

          end;

            suppose

             A100: ((k + 1) + 1) = d & for i holds (r . i) < (l . i) & [(l . i), (r . i)] is Gap of (G . i);

            then

             A101: A = ( infinite-cell G) by A98, Th46;

            set C = ( {A} ` );

            

             A102: for A be 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

               A103: A9 <> ( infinite-cell G) by A101, TARSKI:def 1;

              consider l9, r9 such that

               A104: A9 = ( cell (l9,r9)) and

               A105: (ex X be 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, Th29;

              per cases by A105;

                suppose ex X be 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, A104;

              end;

                suppose for i holds (r9 . i) < (l9 . i) & [(l9 . i), (r9 . i)] is Gap of (G . i);

                hence thesis by A103, A104, Th46;

              end;

            end;

            

             A106: for C1,C2 be Chain of ((k + 1) + 1), G st C1 c= C & C2 c= C & P[C1] & P[C2] holds P[(C1 + C2)] by A94;

             P[C] from ChainInd( A97, A102, A106);

            hence thesis by A100, Th59;

          end;

        end;

        then

         A107: for A be Cell of ((k + 1) + 1), G st A in C holds P[ {A}];

        

         A108: for C1,C2 be Chain of ((k + 1) + 1), G st C1 c= C & C2 c= C & P[C1] & P[C2] holds P[(C1 + C2)] by A94;

        thus P[C] from ChainInd( A97, A107, A108);

      end;

        suppose ((k + 1) + 1) > d;

        then ( del C) = ( 0_ ((k + 1),G)) by Th49;

        hence thesis by Th56;

      end;

    end;

    definition

      let d, G, k;

      :: CHAIN_1:def14

      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 be 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 be Nat st k = (k9 + 1);

          then

          consider k9 be 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, Th56;

          end;

          hence thesis;

        end;

      end;

    end

    theorem :: CHAIN_1:64

    

     Th61: for C be 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 be 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 :: CHAIN_1:65

    k > d implies for C be 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 be 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, Th49;

      hence thesis by A2, Def14;

    end;

    theorem :: CHAIN_1:66

    

     Th63: for C be 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 be 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;

      :: original: del

      redefine

      :: CHAIN_1:def15

      func del C equals ( 0_ (k,G));

      compatibility by Th61;

    end

    definition

      let d, G, k;

      :: original: 0_

      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 be Nat st k = (k9 + 1);

          then

          consider k9 be 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 Th56;

          hence thesis by A2, Def14;

        end;

      end;

    end

    definition

      let d, G;

      :: original: Omega

      redefine

      func Omega (G) -> Cycle of d, G ;

      coherence

      proof

        consider d9 be 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 Th57;

        hence thesis by A1, Def14;

      end;

    end

    definition

      let d, G, k;

      let C1,C2 be Cycle of k, G;

      :: original: +

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

          ( card C2) is even by A1, Th63;

          then ( card (C1 + C2)) is even by A2, Th7;

          hence (C1 + C2) is Cycle of k, G by A1, Th63;

        end;

          suppose ex k9 be Nat st k = (k9 + 1);

          then

          consider k9 be 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, Th58

          .= ( 0_ (k9,G));

          hence thesis by A3, Th61;

        end;

      end;

    end

    theorem :: CHAIN_1:67

    for C be Cycle of d, G holds (C ` ) is Cycle of d, G

    proof

      let C be Cycle of d, G;

      consider d9 be 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 Th59;

      hence thesis by A1, Th61;

    end;

    definition

      let d, G, k;

      let C be Chain of (k + 1), G;

      :: original: del

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

            hence ( del {B}) is Cycle of 0 , G by Def14;

          end;

          then

           A3: for A be Cell of (k + 1), G st A in C holds P[ {A}] by A1;

          

           A4: for C1,C2 be 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 Th58;

            hence thesis;

          end;

          thus P[C] from ChainInd( A2, A3, A4);

        end;

          suppose ex k9 be Nat st k = (k9 + 1);

          then

          consider k9 be 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 Th60;

          hence thesis by A7, Th61;

        end;

      end;

    end

    begin

    definition

      let d, G, k;

      :: CHAIN_1:def16

      func Chains (k,G) -> strict AbGroup means

      : Def16: the carrier of it = ( bool ( cells (k,G))) & ( 0. it ) = ( 0_ (k,G)) & for A,B be Element of it , A9,B9 be 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 be BinOp of ( bool ( cells (k,G))) such that

         A1: for A,B be 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 be Element of C1, A9,B9 be 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 be Element of C2, A9,B9 be 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 be 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 :: CHAIN_1:68

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

    definition

      let d, G, k;

      :: CHAIN_1:def17

      func del (k,G) -> Homomorphism of ( Chains ((k + 1),G)), ( Chains (k,G)) means for A be Element of ( Chains ((k + 1),G)), A9 be 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 be Function of ( bool ( cells ((k + 1),G))), ( bool ( cells (k,G))) such that

         A1: for A be 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 be 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 Th58

          .= (( 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 be Element of ( Chains ((k + 1),G)), A9 be Chain of (k + 1), G st A = A9 holds (f . A) = ( del A9);

        assume

         A4: for A be Element of ( Chains ((k + 1),G)), A9 be 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