let k be Element of NAT ; :: thesis:
let d be non zero Element of 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

let A be set ; :: 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

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, Th51, Th54; :: thesis:

end;

A9: not card ((star A) /\ (del {C})) is even by A7, Th52;
consider B being set 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, XBOOLE_1:1;
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, Th34;
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, Th33;
l9 . the Element of Seg d <= r9 . the Element of Seg d by A5, A6, A12, A15, Th29;
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, Th48;
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 Th6;
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, 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 Real st S₁[i,xi]

proof

let i be Element of Seg d; :: thesis:
( i in X \/ {i1} or not i in X \/ {i1} ) ;
hence ex xi being Real st S₁[i,xi] ; :: thesis:

end;

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

proof

let i be Element of Seg d; :: thesis:
( i in X \/ {i1} or not i in X \/ {i1} ) ;
hence ex xi being Real st S₂[i,xi] ; :: thesis:

end;

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

proof

let i be Element of Seg d; :: thesis:
( i in X \/ {i1} or not i in X \/ {i1} ) ;
then ( ( l1 . i = l . i & r1 . i = r . i ) or ( l1 . i = l9 . i & r1 . i = r9 . i ) ) by A31, A33;
hence l1 . i <= r1 . i by A14, A18; :: thesis:

end;

A35: 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 A36: i in X \/ {i1} ; :: thesis:

then A37: l1 . i = l . i by A31;
r1 . i = r . i by A33, A36;
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, A36, A37; :: thesis:

end;

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

then A39: l1 . i = l9 . i by A31;
A40: r1 . i = r9 . i by A33, A38;
not i in X by A28, 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 A18, A38, A39, A40; :: thesis:

end;

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

proof

let i be Element of Seg d; :: thesis:
( i in X \/ {i2} or not i in X \/ {i2} ) ;
hence ex xi being Real st S₃[i,xi] ; :: thesis:

end;

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

proof

let i be Element of Seg d; :: thesis:
( i in X \/ {i2} or not i in X \/ {i2} ) ;
hence ex xi being Real st S₄[i,xi] ; :: thesis:

end;

consider r2 being Function of (Seg d),REAL such that
A46: for i being Element of Seg d holds S₄[i,r2 . i] from FUNCT_2:sch 3(A45);
reconsider l2 = l2, r2 = r2 as Element of REAL d by Def4;
A47: 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 A48: i in X \/ {i2} ; :: thesis:

then A49: l2 . i = l . i by A44;
r2 . i = r . i by A46, A48;
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, A42, A48, A49; :: thesis:

end;

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

then A51: l2 . i = l9 . i by A44;
A52: r2 . i = r9 . i by A46, A50;
not i in X by A41, A50;
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, A50, A51, A52; :: thesis:

end;

then reconsider B2 = cell (l2,r2) as Cell of (k + 1),G by A2, A47, Th34;
take B1 ; :: thesis:
take B2 ; :: thesis:
A53: 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 A54: i in X \/ {i1} ; :: thesis:

then A55: l1 . i = l . i by A31;
r1 . i = r . i by A33, A54;
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, A55, Th29; :: thesis:

end;

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

then A57: l1 . i = l9 . i by A31;
r1 . i = r9 . i by A33, A56;
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, A57, Th29; :: thesis:

end;

then A58: A c= B1 by A15, Th29;
B1 c= C by A5, A6, A53, Th29;
hence B1 in (star A) /\ (del {C}) by A8, A58; :: thesis:
A59: 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 A60: i in X \/ {i2} ; :: thesis:

then A61: l2 . i = l . i by A44;
r2 . i = r . i by A46, A60;
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, A61, Th29; :: thesis:

end;

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

then A63: l2 . i = l9 . i by A44;
r2 . i = r9 . i by A46, A62;
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, A63, Th29; :: thesis:

end;

then A64: A c= B2 by A15, Th29;
B2 c= C by A5, A6, A59, Th29;
hence B2 in (star A) /\ (del {C}) by A8, A64; :: thesis:
i1 in {i1} by TARSKI:def 1;
then A65: i1 in X \/ {i1} by XBOOLE_0:def 3;
A66: not i1 in X by A20, XBOOLE_0:def 5;
not i1 in {i2} by A22, TARSKI:def 1;
then A67: not i1 in X \/ {i2} by A66, XBOOLE_0:def 3;
A68: l1 . i1 = l . i1 by A31, A65;
A69: r1 . i1 = r . i1 by A33, A65;
A70: l2 . i1 = l9 . i1 by A44, A67;
A71: r2 . i1 = r9 . i1 by A46, A67;
l . i1 < r . i1 by A14, A24;
then ( l1 <> l2 or r1 <> r2 ) by A18, A26, A68, A69, A70, A71;
hence B1 <> B2 by A34, Th32; :: thesis:
let B be set ; :: thesis:
assume A72: B in (star A) /\ (del {C}) ; :: thesis:
then reconsider B = B as Cell of (k + 1),G ;
A73: A c= B by A8, A72;
A74: B c= C by A8, A72;
consider l99, r99 being Element of REAL d such that
A75: B = cell (l99,r99) and
A76: ( 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, Th33;
l99 . the Element of Seg d <= r99 . the Element of Seg d by A5, A6, A74, A75, Th29;
then consider Y being Subset of (Seg d) such that
A77: card Y = k + 1 and
A78: 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 A76;
A79: X c= Y by A15, A18, A73, A75, A78, Th48;
A80: Y c= Z by A5, A14, A74, A75, A78, Th48;
card (Y \ X) = (k + 1) - k by A17, A77, A79, CARD_2:44
.= 1 ;
then consider i9 being set such that
A81: Y \ X = {i9} by CARD_2:42;
A82: i9 in Y \ X by A81, TARSKI:def 1;
then reconsider i9 = i9 as Element of Seg d ;
A83: i9 in Y by A82, XBOOLE_0:def 5;
not i9 in X by A82, XBOOLE_0:def 5;
then A84: i9 in Z \ X by A80, A83, XBOOLE_0:def 5;
A85: Y = X \/ Y by A79, XBOOLE_1:12
.= X \/ {i9} by A81, XBOOLE_1:39 ;

per cases by A23, A84, A85;

suppose A86: Y = X \/ {i1} ; :: thesis:

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

A87: now

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, A31, A33, A73, A74, A75, A78, A86, Th48;
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 A75, A87, FUNCT_2:63; :: thesis:

end;

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

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

A89: now

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, A44, A46, A73, A74, A75, A78, A88, Th48;
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 A75, A89, FUNCT_2:63; :: thesis:

end;

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

end;

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

end;

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

proof

let C1, C2 be Chain of ((k + 1) + 1),G; :: thesis:
assume that
A91: del (del C1) = 0_ (k,G) and
A92: del (del C2) = 0_ (k,G) ; :: thesis:
thus del (del (C1 + C2)) = del ((del C1) + (del C2)) by Th63
.= (0_ (k,G)) + (0_ (k,G)) by A91, A92, Th63
.= 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 Th61
.= 0_ (k,G) by Th61 ;
then A93: 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
A94: A = cell (l,r) and
A95: ( 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, Th33;

per cases by A95;

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, A94; :: thesis:

end;

suppose A96: ( (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 A97: A = infinite-cell G by A94, Th50;
set C = {A} ` ;
A98: 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 A99: A9 <> infinite-cell G by A97, TARSKI:def 1;
consider l9, r9 being Element of REAL d such that
A100: A9 = cell (l9,r9) and
A101: ( 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, Th33;

per cases by A101;

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, A100; :: 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 A99, A100, Th50; :: thesis:

end;

A102: 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 A90;
S₁[{A} ` ] from CHAIN_1:sch 4(A93, A98, A102);
hence del (del {A}) = 0_ (k,G) by A96, Th64; :: thesis:

end;

then A103: for A being Cell of ((k + 1) + 1),G st A in C holds
S₁[{A}] ;
A104: 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 A90;
thus S₁[C] from CHAIN_1:sch 4(A93, A103, A104); :: thesis:

end;

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

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

end;