let k be Nat; :: thesis: for d being non zero Nat
for G being Grating of d
for C being Chain of ((k + 1) + 1),G holds del (del C) = 0_ (k,G)

let d be non zero Nat; :: thesis: for G being Grating of d
for C being Chain of ((k + 1) + 1),G holds del (del C) = 0_ (k,G)

let G be Grating of d; :: thesis: for C being Chain of ((k + 1) + 1),G holds del (del C) = 0_ (k,G)
let C be Chain of ((k + 1) + 1),G; :: thesis: del (del C) = 0_ (k,G)
per cases ) + 1 <= d or (k + 1) + 1 > d ) ;
suppose A1: (k + 1) + 1 <= d ; :: thesis: del (del C) = 0_ (k,G)
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 () = 0_ (k,G)
proof
let C be Cell of ((k + 1) + 1),G; :: thesis: 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 () = 0_ (k,G)

let l, r be Element of REAL d; :: thesis: ( C = cell (l,r) & ( for i being Element of Seg d holds l . i <= r . i ) implies del () = 0_ (k,G) )
assume that
A5: C = cell (l,r) and
A6: for i being Element of Seg d holds l . i <= r . i ; :: thesis: del () = 0_ (k,G)
now :: thesis: for A being object holds not A in del ()
let A be object ; :: thesis: not A in del ()
assume A7: A in del () ; :: thesis: contradiction
then reconsider A = A as Cell of k,G ;
set BB = (star A) /\ ();
A8: now :: thesis: for B being Cell of (k + 1),G holds
( B in (star A) /\ () iff ( A c= B & B c= C ) )
let B be Cell of (k + 1),G; :: thesis: ( B in (star A) /\ () iff ( A c= B & B c= C ) )
( B in (star A) /\ () iff ( B in star A & B in del {C} ) ) by XBOOLE_0:def 4;
hence ( B in (star A) /\ () iff ( A c= B & B c= C ) ) by ; :: thesis: verum
end;
A9: card ((star A) /\ ()) is odd by ;
consider B being object such that
A10: B in (star A) /\ () by ;
reconsider B = B as Cell of (k + 1),G by A10;
A11: A c= B by ;
B c= C by ;
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 ;
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) /\ () & B2 in (star A) /\ () & B1 <> B2 & ( for B being set holds
( not B in (star A) /\ () 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
.= 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 ;
A25: i2 in Z by ;
A26: not i1 in X by ;
A27: not i2 in X by ;
reconsider i1 = i1, i2 = i2 as Element of Seg d by ;
set Y1 = X \/ {i1};
A28: X c= X \/ {i1} by XBOOLE_1:7;
{i1} c= Z by ;
then A29: X \/ {i1} c= Z by ;
defpred S1[ 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 S1[i,xi]
proof
let i be Element of Seg d; :: thesis: ex xi being Element of REAL st S1[i,xi]
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 S1[i,xi] by A31; :: thesis: verum
end;
consider l1 being Function of (Seg d),REAL such that
A32: for i being Element of Seg d holds S1[i,l1 . i] from defpred S2[ 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 S2[i,xi]
proof
let i be Element of Seg d; :: thesis: ex xi being Element of REAL st S2[i,xi]
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 S2[i,xi] by A34; :: thesis: verum
end;
consider r1 being Function of (Seg d),REAL such that
A35: for i being Element of Seg d holds S2[i,r1 . i] from 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 <= r1 . i
( ( l1 . i = l . i & r1 . i = r . i ) or ( l1 . i = l9 . i & r1 . i = r9 . i ) ) by ;
hence l1 . i <= r1 . i by ; :: thesis: verum
end;
A37: card (X \/ {i1}) = (card X) + (card {i1}) by
.= k + 1 by ;
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: ( ( 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 ) )
per cases ( i in X \/ {i1} or not i in X \/ {i1} ) ;
suppose A38: i in X \/ {i1} ; :: thesis: ( ( 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 ) )
then A39: l1 . i = l . i by A32;
r1 . i = r . i by ;
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: verum
end;
suppose A40: not i in X \/ {i1} ; :: thesis: ( ( 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 ) )
then A41: l1 . i = l9 . i by A32;
A42: r1 . i = r9 . i by ;
not i in X by ;
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: verum
end;
end;
end;
then reconsider B1 = cell (l1,r1) as Cell of (k + 1),G by ;
set Y2 = X \/ {i2};
A43: X c= X \/ {i2} by XBOOLE_1:7;
{i2} c= Z by ;
then A44: X \/ {i2} c= Z by ;
defpred S3[ 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 S3[i,xi]
proof
let i be Element of Seg d; :: thesis: ex xi being Element of REAL st S3[i,xi]
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 S3[i,xi] by A46; :: thesis: verum
end;
consider l2 being Function of (Seg d),REAL such that
A47: for i being Element of Seg d holds S3[i,l2 . i] from defpred S4[ 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 S4[i,xi]
proof
let i be Element of Seg d; :: thesis: ex xi being Element of REAL st S4[i,xi]
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 S4[i,xi] by A49; :: thesis: verum
end;
consider r2 being Function of (Seg d),REAL such that
A50: for i being Element of Seg d holds S4[i,r2 . i] from reconsider l2 = l2, r2 = r2 as Element of REAL d by Def3;
A51: card (X \/ {i2}) = (card X) + (card {i2}) by
.= k + 1 by ;
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: ( ( 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 ) )
per cases ( i in X \/ {i2} or not i in X \/ {i2} ) ;
suppose A52: i in X \/ {i2} ; :: thesis: ( ( 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 ) )
then A53: l2 . i = l . i by A47;
r2 . i = r . i by ;
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: verum
end;
suppose A54: not i in X \/ {i2} ; :: thesis: ( ( 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 ) )
then A55: l2 . i = l9 . i by A47;
A56: r2 . i = r9 . i by ;
not i in X by ;
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: verum
end;
end;
end;
then reconsider B2 = cell (l2,r2) as Cell of (k + 1),G by ;
take B1 ; :: thesis: ex B2 being set st
( B1 in (star A) /\ () & B2 in (star A) /\ () & B1 <> B2 & ( for B being set holds
( not B in (star A) /\ () or B = B1 or B = B2 ) ) )

take B2 ; :: thesis: ( B1 in (star A) /\ () & B2 in (star A) /\ () & B1 <> B2 & ( for B being set holds
( not B in (star A) /\ () or B = B1 or B = B2 ) ) )

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: ( l1 . i <= l9 . i & l9 . i <= r9 . i & r9 . i <= r1 . i & l . i <= l1 . i & l1 . i <= r1 . i & r1 . i <= r . i )
per cases ( i in X \/ {i1} or not i in X \/ {i1} ) ;
suppose A58: i in X \/ {i1} ; :: thesis: ( l1 . i <= l9 . i & l9 . i <= r9 . i & r9 . i <= r1 . i & l . i <= l1 . i & l1 . i <= r1 . i & r1 . i <= r . i )
then A59: l1 . i = l . i by A32;
r1 . i = r . i by ;
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: verum
end;
suppose A60: not i in X \/ {i1} ; :: thesis: ( l1 . i <= l9 . i & l9 . i <= r9 . i & r9 . i <= r1 . i & l . i <= l1 . i & l1 . i <= r1 . i & r1 . i <= r . i )
then A61: l1 . i = l9 . i by A32;
r1 . i = r9 . i by ;
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: verum
end;
end;
end;
then A62: A c= B1 by ;
B1 c= C by A5, A6, A57, Th25;
hence B1 in (star A) /\ () by ; :: thesis: ( B2 in (star A) /\ () & B1 <> B2 & ( for B being set holds
( not B in (star A) /\ () or B = B1 or B = B2 ) ) )

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: ( l2 . i <= l9 . i & l9 . i <= r9 . i & r9 . i <= r2 . i & l . i <= l2 . i & l2 . i <= r2 . i & r2 . i <= r . i )
per cases ( i in X \/ {i2} or not i in X \/ {i2} ) ;
suppose A64: i in X \/ {i2} ; :: thesis: ( l2 . i <= l9 . i & l9 . i <= r9 . i & r9 . i <= r2 . i & l . i <= l2 . i & l2 . i <= r2 . i & r2 . i <= r . i )
then A65: l2 . i = l . i by A47;
r2 . i = r . i by ;
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: verum
end;
suppose A66: not i in X \/ {i2} ; :: thesis: ( l2 . i <= l9 . i & l9 . i <= r9 . i & r9 . i <= r2 . i & l . i <= l2 . i & l2 . i <= r2 . i & r2 . i <= r . i )
then A67: l2 . i = l9 . i by A47;
r2 . i = r9 . i by ;
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: verum
end;
end;
end;
then A68: A c= B2 by ;
B2 c= C by A5, A6, A63, Th25;
hence B2 in (star A) /\ () by ; :: thesis: ( B1 <> B2 & ( for B being set holds
( not B in (star A) /\ () or B = B1 or B = B2 ) ) )

i1 in {i1} by TARSKI:def 1;
then A69: i1 in X \/ {i1} by XBOOLE_0:def 3;
A70: not i1 in X by ;
not i1 in {i2} by ;
then A71: not i1 in X \/ {i2} by ;
A72: l1 . i1 = l . i1 by ;
A73: r1 . i1 = r . i1 by ;
A74: l2 . i1 = l9 . i1 by ;
A75: r2 . i1 = r9 . i1 by ;
l . i1 < r . i1 by ;
then ( l1 <> l2 or r1 <> r2 ) by A18, A26, A72, A73, A74, A75;
hence B1 <> B2 by ; :: thesis: for B being set holds
( not B in (star A) /\ () or B = B1 or B = B2 )

let B be set ; :: thesis: ( not B in (star A) /\ () or B = B1 or B = B2 )
assume A76: B in (star A) /\ () ; :: thesis: ( B = B1 or B = B2 )
then reconsider B = B as Cell of (k + 1),G ;
A77: A c= B by ;
A78: B c= C by ;
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 ;
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
.= 1 ;
then consider i9 being object such that
A85: Y \ X = {i9} by CARD_2:42;
A86: i9 in Y \ X by ;
then reconsider i9 = i9 as Element of Seg d ;
A87: i9 in Y by ;
not i9 in X by ;
then A88: i9 in Z \ X by ;
A89: Y = X \/ Y by
.= X \/ {i9} by ;
per cases ( Y = X \/ {i1} or Y = X \/ {i2} ) by ;
suppose A90: Y = X \/ {i1} ; :: thesis: ( B = B1 or B = B2 )
reconsider l99 = l99, r99 = r99, l1 = l1, r1 = r1 as Function of (Seg d),REAL by Def3;
A91: now :: thesis: for i being Element of Seg d holds
( l99 . i = l1 . i & r99 . i = r1 . i )
let i be Element of Seg d; :: thesis: ( l99 . i = l1 . i & r99 . i = r1 . 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 ) ; :: thesis: verum
end;
then l99 = l1 by FUNCT_2:63;
hence ( B = B1 or B = B2 ) by ; :: thesis: verum
end;
suppose A92: Y = X \/ {i2} ; :: thesis: ( B = B1 or B = B2 )
reconsider l99 = l99, r99 = r99, l2 = l2, r2 = r2 as Function of (Seg d),REAL by Def3;
A93: now :: thesis: for i being Element of Seg d holds
( l99 . i = l2 . i & r99 . i = r2 . i )
let i be Element of Seg d; :: thesis: ( l99 . i = l2 . i & r99 . i = r2 . 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 ) ; :: thesis: verum
end;
then l99 = l2 by FUNCT_2:63;
hence ( B = B1 or B = B2 ) by ; :: thesis: verum
end;
end;
end;
then card ((star A) /\ ()) = 2 * 1 by Th5;
hence contradiction by A7, Th48; :: thesis: verum
end;
hence del () = 0_ (k,G) by XBOOLE_0:def 1; :: thesis: verum
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: ( del (del C1) = 0_ (k,G) & del (del C2) = 0_ (k,G) implies del (del (C1 + C2)) = 0_ (k,G) )
assume that
A95: del (del C1) = 0_ (k,G) and
A96: del (del C2) = 0_ (k,G) ; :: thesis: del (del (C1 + C2)) = 0_ (k,G)
thus del (del (C1 + C2)) = del ((del C1) + (del C2)) by Th58
.= (0_ (k,G)) + (0_ (k,G)) by
.= 0_ (k,G) ; :: thesis: verum
end;
defpred S1[ 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: S1[ 0_ (((k + 1) + 1),G)] ;
for A being Cell of ((k + 1) + 1),G holds del () = 0_ (k,G)
proof
let A be Cell of ((k + 1) + 1),G; :: thesis: del () = 0_ (k,G)
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 ;
per cases ( 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 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: del () = 0_ (k,G)
then for i being Element of Seg d holds l . i <= r . i ;
hence del () = 0_ (k,G) by ; :: thesis: verum
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: del () = 0_ (k,G)
then A101: A = infinite-cell G by ;
set C = {A} ` ;
A102: for A being Cell of ((k + 1) + 1),G st A in {A} ` holds
S1[{A}]
proof
let A9 be Cell of ((k + 1) + 1),G; :: thesis: ( A9 in {A} ` implies S1[{A9}] )
assume A9 in {A} ` ; :: thesis: S1[{A9}]
then not A9 in {A} by XBOOLE_0:def 5;
then A103: A9 <> infinite-cell G by ;
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 ;
per cases ( 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 for i being Element of Seg d holds
( r9 . i < l9 . i & [(l9 . i),(r9 . i)] is Gap of G . i ) )
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: S1[{A9}]
then for i being Element of Seg d holds l9 . i <= r9 . i ;
hence S1[{A9}] by ; :: thesis: verum
end;
suppose for i being Element of Seg d holds
( r9 . i < l9 . i & [(l9 . i),(r9 . i)] is Gap of G . i ) ; :: thesis: S1[{A9}]
hence S1[{A9}] by ; :: thesis: verum
end;
end;
end;
A106: for C1, C2 being Chain of ((k + 1) + 1),G st C1 c= {A} ` & C2 c= {A} ` & S1[C1] & S1[C2] holds
S1[C1 + C2] by A94;
S1[{A} ` ] from hence del () = 0_ (k,G) by ; :: thesis: verum
end;
end;
end;
then A107: for A being Cell of ((k + 1) + 1),G st A in C holds
S1[{A}] ;
A108: for C1, C2 being Chain of ((k + 1) + 1),G st C1 c= C & C2 c= C & S1[C1] & S1[C2] holds
S1[C1 + C2] by A94;
thus S1[C] from CHAIN_1:sch 4(A97, A107, A108); :: thesis: verum
end;
suppose (k + 1) + 1 > d ; :: thesis: del (del C) = 0_ (k,G)
then del C = 0_ ((k + 1),G) by Th49;
hence del (del C) = 0_ (k,G) by Th56; :: thesis: verum
end;
end;