let k be Nat; :: thesis:
let d be non zero Nat; :: thesis:
let G be Grating of d; :: thesis:
let C be Chain of ((k + 1) + 1),G; :: thesis:

per cases ) + 1 <= d or (k + 1) + 1 > d ) ;

suppose A1: (k + 1) + 1 <= d ; :: thesis:

then A2: k + 1 < d by NAT_1:13;
then A3: k < d by NAT_1:13;
A4: for C being Cell of ((k + 1) + 1),G
for l, r being Element of REAL d st C = cell (l,r) & ( for i being Element of Seg d holds l . i <= r . i ) holds
del (del {C}) = 0_ (k,G)

proof

let C be Cell of ((k + 1) + 1),G; :: thesis:
let l, r be Element of REAL d; :: thesis:
assume that
A5: C = cell (l,r) and
A6: for i being Element of Seg d holds l . i <= r . i ; :: thesis:

now :: thesis:

let A be object ; :: thesis:
assume A7: A in del (del {C}) ; :: thesis:
then reconsider A = A as Cell of k,G ;
set BB = (star A) /\ (del {C});

A8: now :: thesis:

let B be Cell of (k + 1),G; :: thesis:
( B in (star A) /\ (del {C}) iff ( B in star A & B in del {C} ) ) by XBOOLE_0:def 4;
hence ( B in (star A) /\ (del {C}) iff ( A c= B & B c= C ) ) by A1, Th47, Th50; :: thesis:

end;

A9: card ((star A) /\ (del {C})) is odd by A7, Th48;
consider B being object such that
A10: B in (star A) /\ (del {C}) by A9, CARD_1:27, XBOOLE_0:def 1;
reconsider B = 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 . the Element of Seg d <= r . the Element of Seg d by A6;
then consider Z being Subset of (Seg d) such that
A13: card Z = (k + 1) + 1 and
A14: for i being Element of Seg d 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 being Element of REAL d such that
A15: A = cell (l9,r9) and
A16: ( ex X being Subset of (Seg d) st
( card X = k & ( for i being Element of Seg d 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 being Element of Seg d holds
( r9 . i < l9 . i & [(l9 . i),(r9 . i)] is Gap of G . i ) ) ) ) by A3, Th29;
l9 . the Element of Seg d <= r9 . the Element of Seg d by A5, A6, A12, A15, Th25;
then consider X being Subset of (Seg d) such that
A17: card X = k and
A18: for i being Element of Seg d holds
( ( i in X & l9 . i < r9 . i & [(l9 . i),(r9 . i)] is Gap of G . i ) or ( not i in X & l9 . i = r9 . i & l9 . i in G . i ) ) by A16;
ex B1, B2 being set st
( B1 in (star A) /\ (del {C}) & B2 in (star A) /\ (del {C}) & B1 <> B2 & ( for B being set holds
( not B in (star A) /\ (del {C}) or 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 being set such that
A20: i1 in Z \ X and
A21: i2 in Z \ X and
A22: i1 <> i2 and
A23: for i being set holds
( not i in Z \ X or 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 = i1, i2 = i2 as Element of Seg d by A20, A21;
set Y1 = X \/ {i1};
A28: X c= X \/ {i1} by XBOOLE_1:7;
{i1} c= Z by A24, ZFMISC_1:31;
then A29: X \/ {i1} c= Z by A19, XBOOLE_1:8;
defpred S₁[ Element of Seg d, Element of REAL ] means ( ( $1 in X \/ {i1} implies $2 = l . $1 ) & ( not $1 in X \/ {i1} implies $2 = l9 . $1 ) );
A30: for i being Element of Seg d ex xi being Element of REAL st S₁[i,xi]

proof

let i be Element of Seg d; :: thesis:
A31: ( l . i in REAL & l9 . i in REAL ) by XREAL_0:def 1;
( i in X \/ {i1} or not i in X \/ {i1} ) ;
hence ex xi being Element of REAL st S₁[i,xi] by A31; :: thesis:

end;

consider l1 being Function of (Seg d),REAL such that
A32: for i being Element of Seg d holds S₁[i,l1 . i] from FUNCT_2:sch 3(A30);
defpred S₂[ Element of Seg d, Element of REAL ] means ( ( $1 in X \/ {i1} implies $2 = r . $1 ) & ( not $1 in X \/ {i1} implies $2 = r9 . $1 ) );
A33: for i being Element of Seg d ex xi being Element of REAL st S₂[i,xi]

proof

let i be Element of Seg d; :: thesis:
A34: ( r . i in REAL & r9 . i in REAL ) by XREAL_0:def 1;
( i in X \/ {i1} or not i in X \/ {i1} ) ;
hence ex xi being Element of REAL st S₂[i,xi] by A34; :: thesis:

end;

consider r1 being Function of (Seg d),REAL such that
A35: for i being Element of Seg d holds S₂[i,r1 . i] from FUNCT_2:sch 3(A33);
reconsider l1 = l1, r1 = r1 as Element of REAL d by Def3;
A36: for i being Element of Seg d holds l1 . i <= r1 . i

proof

let i be Element of Seg d; :: thesis:
( ( l1 . i = l . i & r1 . i = r . i ) or ( l1 . i = l9 . i & r1 . i = r9 . i ) ) by A32, A35;
hence l1 . i <= r1 . i by A14, A18; :: thesis:

end;

A37: card (X \/ {i1}) = (card X) + (card {i1}) by A26, CARD_2:40, ZFMISC_1:50
.= k + 1 by A17, CARD_1:30 ;
for i being Element of Seg d holds
( ( i in X \/ {i1} & l1 . i < r1 . i & [(l1 . i),(r1 . i)] is Gap of G . i ) or ( not i in X \/ {i1} & l1 . i = r1 . i & l1 . i in G . i ) )

proof

let i be Element of Seg d; :: thesis:

per cases ;

suppose A38: i in X \/ {i1} ; :: thesis:

then A39: l1 . i = l . i by A32;
r1 . i = r . i by A35, A38;
hence ( ( i in X \/ {i1} & l1 . i < r1 . i & [(l1 . i),(r1 . i)] is Gap of G . i ) or ( not i in X \/ {i1} & l1 . i = r1 . i & l1 . i in G . i ) ) by A14, A29, A38, A39; :: thesis:

end;

suppose A40: not i in X \/ {i1} ; :: thesis:

then A41: l1 . i = l9 . i by A32;
A42: r1 . i = r9 . i by A35, A40;
not i in X by A28, A40;
hence ( ( i in X \/ {i1} & l1 . i < r1 . i & [(l1 . i),(r1 . i)] is Gap of G . i ) or ( not i in X \/ {i1} & l1 . i = r1 . i & l1 . i in G . i ) ) by A18, A40, A41, A42; :: thesis:

end;

then reconsider B1 = cell (l1,r1) as Cell of (k + 1),G by A2, A37, Th30;
set Y2 = X \/ {i2};
A43: X c= X \/ {i2} by XBOOLE_1:7;
{i2} c= Z by A25, ZFMISC_1:31;
then A44: X \/ {i2} c= Z by A19, XBOOLE_1:8;
defpred S₃[ Element of Seg d, Element of REAL ] means ( ( $1 in X \/ {i2} implies $2 = l . $1 ) & ( not $1 in X \/ {i2} implies $2 = l9 . $1 ) );
A45: for i being Element of Seg d ex xi being Element of REAL st S₃[i,xi]

proof

let i be Element of Seg d; :: thesis:
A46: ( l . i in REAL & l9 . i in REAL ) by XREAL_0:def 1;
( i in X \/ {i2} or not i in X \/ {i2} ) ;
hence ex xi being Element of REAL st S₃[i,xi] by A46; :: thesis:

end;

consider l2 being Function of (Seg d),REAL such that
A47: for i being Element of Seg d holds S₃[i,l2 . i] from FUNCT_2:sch 3(A45);
defpred S₄[ Element of Seg d, Element of REAL ] means ( ( $1 in X \/ {i2} implies $2 = r . $1 ) & ( not $1 in X \/ {i2} implies $2 = r9 . $1 ) );
A48: for i being Element of Seg d ex xi being Element of REAL st S₄[i,xi]

proof

let i be Element of Seg d; :: thesis:
A49: ( r . i in REAL & r9 . i in REAL ) by XREAL_0:def 1;
( i in X \/ {i2} or not i in X \/ {i2} ) ;
hence ex xi being Element of REAL st S₄[i,xi] by A49; :: thesis:

end;

consider r2 being Function of (Seg d),REAL such that
A50: for i being Element of Seg d holds S₄[i,r2 . i] from FUNCT_2:sch 3(A48);
reconsider l2 = l2, r2 = r2 as Element of REAL d by Def3;
A51: card (X \/ {i2}) = (card X) + (card {i2}) by A27, CARD_2:40, ZFMISC_1:50
.= k + 1 by A17, CARD_1:30 ;
for i being Element of Seg d holds
( ( i in X \/ {i2} & l2 . i < r2 . i & [(l2 . i),(r2 . i)] is Gap of G . i ) or ( not i in X \/ {i2} & l2 . i = r2 . i & l2 . i in G . i ) )

proof

let i be Element of Seg d; :: thesis:

per cases ;

suppose A52: i in X \/ {i2} ; :: thesis:

then A53: l2 . i = l . i by A47;
r2 . i = r . i by A50, A52;
hence ( ( i in X \/ {i2} & l2 . i < r2 . i & [(l2 . i),(r2 . i)] is Gap of G . i ) or ( not i in X \/ {i2} & l2 . i = r2 . i & l2 . i in G . i ) ) by A14, A44, A52, A53; :: thesis:

end;

suppose A54: not i in X \/ {i2} ; :: thesis:

then A55: l2 . i = l9 . i by A47;
A56: r2 . i = r9 . i by A50, A54;
not i in X by A43, A54;
hence ( ( i in X \/ {i2} & l2 . i < r2 . i & [(l2 . i),(r2 . i)] is Gap of G . i ) or ( not i in X \/ {i2} & l2 . i = r2 . i & l2 . i in G . i ) ) by A18, A54, A55, A56; :: thesis:

end;

then reconsider B2 = cell (l2,r2) as Cell of (k + 1),G by A2, A51, Th30;
take B1 ; :: thesis:
take B2 ; :: thesis:
A57: for i being Element of Seg d 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 be Element of Seg d; :: thesis:

per cases ;

suppose A58: i in X \/ {i1} ; :: thesis:

then A59: l1 . i = l . i by A32;
r1 . i = r . i by A35, A58;
hence ( l1 . i <= l9 . i & l9 . i <= r9 . i & r9 . i <= r1 . i & l . i <= l1 . i & l1 . i <= r1 . i & r1 . i <= r . i ) by A5, A6, A12, A15, A59, Th25; :: thesis:

end;

suppose A60: not i in X \/ {i1} ; :: thesis:

then A61: l1 . i = l9 . i by A32;
r1 . i = r9 . i by A35, A60;
hence ( l1 . i <= l9 . i & l9 . i <= r9 . i & r9 . i <= r1 . i & l . i <= l1 . i & l1 . i <= r1 . i & r1 . i <= r . i ) by A5, A6, A12, A15, A61, Th25; :: thesis:

end;

then A62: A c= B1 by A15, Th25;
B1 c= C by A5, A6, A57, Th25;
hence B1 in (star A) /\ (del {C}) by A8, A62; :: thesis:
A63: for i being Element of Seg d 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 be Element of Seg d; :: thesis:

per cases ;

suppose A64: i in X \/ {i2} ; :: thesis:

then A65: l2 . i = l . i by A47;
r2 . i = r . i by A50, A64;
hence ( l2 . i <= l9 . i & l9 . i <= r9 . i & r9 . i <= r2 . i & l . i <= l2 . i & l2 . i <= r2 . i & r2 . i <= r . i ) by A5, A6, A12, A15, A65, Th25; :: thesis:

end;

suppose A66: not i in X \/ {i2} ; :: thesis:

then A67: l2 . i = l9 . i by A47;
r2 . i = r9 . i by A50, A66;
hence ( l2 . i <= l9 . i & l9 . i <= r9 . i & r9 . i <= r2 . i & l . i <= l2 . i & l2 . i <= r2 . i & r2 . i <= r . i ) by A5, A6, A12, A15, A67, Th25; :: thesis:

end;

then A68: A c= B2 by A15, Th25;
B2 c= C by A5, A6, A63, Th25;
hence B2 in (star A) /\ (del {C}) by A8, A68; :: thesis:
i1 in {i1} by TARSKI:def 1;
then A69: i1 in X \/ {i1} 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 X \/ {i2} 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; :: thesis:
let B be set ; :: thesis:
assume A76: B in (star A) /\ (del {C}) ; :: thesis:
then reconsider B = B as Cell of (k + 1),G ;
A77: A c= B by A8, A76;
A78: B c= C by A8, A76;
consider l99, r99 being Element of REAL d such that
A79: B = cell (l99,r99) and
A80: ( ex Y being Subset of (Seg d) st
( card Y = k + 1 & ( for i being Element of Seg d 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 being Element of Seg d holds
( r99 . i < l99 . i & [(l99 . i),(r99 . i)] is Gap of G . i ) ) ) ) by A2, Th29;
l99 . the Element of Seg d <= r99 . the Element of Seg d by A5, A6, A78, A79, Th25;
then consider Y being Subset of (Seg d) such that
A81: card Y = k + 1 and
A82: for i being Element of Seg d 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 being object such that
A85: Y \ X = {i9} by CARD_2:42;
A86: i9 in Y \ X by A85, TARSKI:def 1;
then reconsider i9 = 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 = X \/ {i1} ; :: thesis:

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

A91: now :: thesis:

let i be Element of Seg d; :: thesis:
( 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 ) ; :: thesis:

end;

then l99 = l1 by FUNCT_2:63;
hence ( B = B1 or B = B2 ) by A79, A91, FUNCT_2:63; :: thesis:

end;

suppose A92: Y = X \/ {i2} ; :: thesis:

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

A93: now :: thesis:

let i be Element of Seg d; :: thesis:
( 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 ) ; :: thesis:

end;

then l99 = l2 by FUNCT_2:63;
hence ( B = B1 or B = B2 ) by A79, A93, FUNCT_2:63; :: thesis:

end;

then card ((star A) /\ (del {C})) = 2 * 1 by Th5;
hence contradiction by A7, Th48; :: thesis:

end;

hence del (del {C}) = 0_ (k,G) by XBOOLE_0:def 1; :: thesis:

end;

A94: for C1, C2 being Chain of ((k + 1) + 1),G st del (del C1) = 0_ (k,G) & del (del C2) = 0_ (k,G) holds
del (del (C1 + C2)) = 0_ (k,G)

proof

let C1, C2 be Chain of ((k + 1) + 1),G; :: thesis:
assume that
A95: del (del C1) = 0_ (k,G) and
A96: del (del C2) = 0_ (k,G) ; :: thesis:
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) ; :: thesis:

end;

defpred S₁[ 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: S₁[ 0_ (((k + 1) + 1),G)] ;
for A being Cell of ((k + 1) + 1),G holds del (del {A}) = 0_ (k,G)

proof

let A be Cell of ((k + 1) + 1),G; :: thesis:
consider l, r being Element of REAL d such that
A98: A = cell (l,r) and
A99: ( ex X being Subset of (Seg d) st
( card X = (k + 1) + 1 & ( for i being Element of Seg d 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 being Element of Seg d holds
( r . i < l . i & [(l . i),(r . i)] is Gap of G . i ) ) ) ) by A1, Th29;

per cases by A99;

suppose ex X being Subset of (Seg d) st
( card X = (k + 1) + 1 & ( for i being Element of Seg d 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 ) ) ) ) ; :: thesis:

then for i being Element of Seg d holds l . i <= r . i ;
hence del (del {A}) = 0_ (k,G) by A4, A98; :: thesis:

end;

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

then A101: A = infinite-cell G by A98, Th46;
set C = {A} ` ;
A102: for A being Cell of ((k + 1) + 1),G st A in {A} ` holds
S₁[{A}]

proof

let A9 be Cell of ((k + 1) + 1),G; :: thesis:
assume A9 in {A} ` ; :: thesis:
then not A9 in {A} by XBOOLE_0:def 5;
then A103: A9 <> infinite-cell G by A101, TARSKI:def 1;
consider l9, r9 being Element of REAL d such that
A104: A9 = cell (l9,r9) and
A105: ( ex X being Subset of (Seg d) st
( card X = (k + 1) + 1 & ( for i being Element of Seg d 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 being Element of Seg d holds
( r9 . i < l9 . i & [(l9 . i),(r9 . i)] is Gap of G . i ) ) ) ) by A1, Th29;

per cases by A105;

suppose ex X being Subset of (Seg d) st
( card X = (k + 1) + 1 & ( for i being Element of Seg d 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 ) ) ) ) ; :: thesis:

then for i being Element of Seg d holds l9 . i <= r9 . i ;
hence S₁[{A9}] by A4, A104; :: thesis:

end;

suppose for i being Element of Seg d holds
( r9 . i < l9 . i & [(l9 . i),(r9 . i)] is Gap of G . i ) ; :: thesis:

hence S₁[{A9}] by A103, A104, Th46; :: thesis:

end;

A106: for C1, C2 being Chain of ((k + 1) + 1),G st C1 c= {A} ` & C2 c= {A} ` & S₁[C1] & S₁[C2] holds
S₁[C1 + C2] by A94;
S₁[{A} ` ] from CHAIN_1:sch 4(A97, A102, A106);
hence del (del {A}) = 0_ (k,G) by A100, Th59; :: thesis:

end;

then A107: for A being Cell of ((k + 1) + 1),G st A in C holds
S₁[{A}] ;
A108: for C1, C2 being Chain of ((k + 1) + 1),G st C1 c= C & C2 c= C & S₁[C1] & S₁[C2] holds
S₁[C1 + C2] by A94;
thus S₁[C] from CHAIN_1:sch 4(A97, A107, A108); :: thesis:

end;

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

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

end;