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)

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
( (k + 1) + 1 <= d or (k + 1) + 1 > d )
;

end;

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 (del {C}) = 0_ (k,G)

del (del (C1 + C2)) = 0_ (k,G)_{1}[ 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_{1}[ 0_ (((k + 1) + 1),G)]
;

for A being Cell of ((k + 1) + 1),G holds del (del {A}) = 0_ (k,G)

S_{1}[{A}]
;

A108: for C1, C2 being Chain of ((k + 1) + 1),G st C1 c= C & C2 c= C & S_{1}[C1] & S_{1}[C2] holds

S_{1}[C1 + C2]
by A94;

thus S_{1}[C]
from CHAIN_1:sch 4(A97, A107, A108); :: thesis: verum

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

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
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 (del {C}) = 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 (del {C}) = 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 (del {C}) = 0_ (k,G)

end;del (del {C}) = 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 (del {C}) = 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 (del {C}) = 0_ (k,G)

now :: thesis: for A being object holds not A in del (del {C})

hence
del (del {C}) = 0_ (k,G)
by XBOOLE_0:def 1; :: thesis: verumlet A be object ; :: thesis: not A in del (del {C})

assume A7: A in del (del {C}) ; :: thesis: contradiction

then reconsider A = A as Cell of k,G ;

set BB = (star A) /\ (del {C});

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 ) ) )

hence contradiction by A7, Th48; :: thesis: verum

end;assume A7: A in del (del {C}) ; :: thesis: contradiction

then reconsider A = A as Cell of k,G ;

set BB = (star A) /\ (del {C});

A8: now :: thesis: for B being Cell of (k + 1),G holds

( B in (star A) /\ (del {C}) iff ( A c= B & B c= C ) )

A9:
card ((star A) /\ (del {C})) is odd
by A7, Th48;( B in (star A) /\ (del {C}) iff ( A c= B & B c= C ) )

let B be Cell of (k + 1),G; :: thesis: ( B in (star A) /\ (del {C}) iff ( A c= B & B c= C ) )

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

end;( 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: verum

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

then
card ((star A) /\ (del {C})) = 2 * 1
by Th5;
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_{1}[ 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_{1}[i,xi]

A32: for i being Element of Seg d holds S_{1}[i,l1 . i]
from FUNCT_2:sch 3(A30);

defpred S_{2}[ 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_{2}[i,xi]

A35: for i being Element of Seg d holds S_{2}[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

.= 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 ) )

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_{3}[ 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_{3}[i,xi]

A47: for i being Element of Seg d holds S_{3}[i,l2 . i]
from FUNCT_2:sch 3(A45);

defpred S_{4}[ 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_{4}[i,xi]

A50: for i being Element of Seg d holds S_{4}[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 ) )

take B1 ; :: thesis: ex 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 ) ) )

take B2 ; :: thesis: ( 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 ) ) )

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 )

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

hence B1 in (star A) /\ (del {C}) by A8, A62; :: thesis: ( 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 ) ) )

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 )

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

hence B2 in (star A) /\ (del {C}) by A8, A68; :: thesis: ( B1 <> B2 & ( for B being set holds

( not B in (star A) /\ (del {C}) 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 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: for B being set holds

( not B in (star A) /\ (del {C}) or B = B1 or B = B2 )

let B be set ; :: thesis: ( not B in (star A) /\ (del {C}) or B = B1 or B = B2 )

assume A76: B in (star A) /\ (del {C}) ; :: thesis: ( B = B1 or B = B2 )

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 ;

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

A30: for i being Element of Seg d ex xi being Element of REAL st S

proof

consider l1 being Function of (Seg d),REAL such that
let i be Element of Seg d; :: thesis: ex xi being Element of REAL st S_{1}[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 S_{1}[i,xi]
by A31; :: thesis: verum

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

A32: for i being Element of Seg d holds S

defpred S

A33: for i being Element of Seg d ex xi being Element of REAL st S

proof

consider r1 being Function of (Seg d),REAL such that
let i be Element of Seg d; :: thesis: ex xi being Element of REAL st S_{2}[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 S_{2}[i,xi]
by A34; :: thesis: verum

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

A35: for i being Element of Seg d holds S

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

A37: card (X \/ {i1}) =
(card X) + (card {i1})
by A26, CARD_2:40, ZFMISC_1:50
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 A32, A35;

hence l1 . i <= r1 . i by A14, A18; :: thesis: verum

end;( ( 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: verum

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

then reconsider B1 = cell (l1,r1) as Cell of (k + 1),G by A2, A37, Th30;
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 ) )

end;per cases
( i in X \/ {i1} or not i in X \/ {i1} )
;

end;

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

end;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: verum

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

end;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: verum

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

A45: for i being Element of Seg d ex xi being Element of REAL st S

proof

consider l2 being Function of (Seg d),REAL such that
let i be Element of Seg d; :: thesis: ex xi being Element of REAL st S_{3}[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 S_{3}[i,xi]
by A46; :: thesis: verum

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

A47: for i being Element of Seg d holds S

defpred S

A48: for i being Element of Seg d ex xi being Element of REAL st S

proof

consider r2 being Function of (Seg d),REAL such that
let i be Element of Seg d; :: thesis: ex xi being Element of REAL st S_{4}[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 S_{4}[i,xi]
by A49; :: thesis: verum

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

A50: for i being Element of Seg d holds S

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

then reconsider B2 = cell (l2,r2) as Cell of (k + 1),G by A2, A51, Th30;
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 ) )

end;per cases
( i in X \/ {i2} or not i in X \/ {i2} )
;

end;

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

end;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: verum

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

end;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: verum

take B1 ; :: thesis: ex 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 ) ) )

take B2 ; :: thesis: ( 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 ) ) )

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

then A62:
A c= B1
by A15, Th25;
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 )

end;per cases
( i in X \/ {i1} or not i in X \/ {i1} )
;

end;

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

end;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: verum

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

end;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: verum

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

hence B1 in (star A) /\ (del {C}) by A8, A62; :: thesis: ( 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 ) ) )

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

then A68:
A c= B2
by A15, Th25;
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 )

end;per cases
( i in X \/ {i2} or not i in X \/ {i2} )
;

end;

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

end;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: verum

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

end;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: verum

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

hence B2 in (star A) /\ (del {C}) by A8, A68; :: thesis: ( B1 <> B2 & ( for B being set holds

( not B in (star A) /\ (del {C}) 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 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: for B being set holds

( not B in (star A) /\ (del {C}) or B = B1 or B = B2 )

let B be set ; :: thesis: ( not B in (star A) /\ (del {C}) or B = B1 or B = B2 )

assume A76: B in (star A) /\ (del {C}) ; :: thesis: ( B = B1 or B = B2 )

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
( Y = X \/ {i1} or Y = X \/ {i2} )
by A23, A88, A89;

end;

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;

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

end;A91: now :: thesis: for i being Element of Seg d holds

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

then
l99 = l1
by FUNCT_2:63;( 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;( 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

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

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;

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

end;A93: now :: thesis: for i being Element of Seg d holds

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

then
l99 = l2
by FUNCT_2:63;( 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;( 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

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

hence contradiction by A7, Th48; :: thesis: verum

del (del (C1 + C2)) = 0_ (k,G)

proof

defpred S
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 A95, A96, Th58

.= 0_ (k,G) ; :: thesis: verum

end;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 A95, A96, Th58

.= 0_ (k,G) ; :: thesis: verum

del (del (0_ (((k + 1) + 1),G))) = del (0_ ((k + 1),G)) by Th56

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

then A97: S

for A being Cell of ((k + 1) + 1),G holds del (del {A}) = 0_ (k,G)

proof

then A107:
for A being Cell of ((k + 1) + 1),G st A in C holds
let A be Cell of ((k + 1) + 1),G; :: thesis: del (del {A}) = 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 A1, Th29;

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

end;

( 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 (del {A}) = 0_ (k,G)

( 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 (del {A}) = 0_ (k,G)

then
for i being Element of Seg d holds l . i <= r . i
;

hence del (del {A}) = 0_ (k,G) by A4, A98; :: thesis: verum

end;hence del (del {A}) = 0_ (k,G) by A4, A98; :: thesis: verum

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 (del {A}) = 0_ (k,G)

( r . i < l . i & [(l . i),(r . i)] is Gap of G . i ) ) ) ; :: thesis: del (del {A}) = 0_ (k,G)

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_{1}[{A}]
_{1}[C1] & S_{1}[C2] holds

S_{1}[C1 + C2]
by A94;

S_{1}[{A} ` ]
from CHAIN_1:sch 4(A97, A102, A106);

hence del (del {A}) = 0_ (k,G) by A100, Th59; :: thesis: verum

end;set C = {A} ` ;

A102: for A being Cell of ((k + 1) + 1),G st A in {A} ` holds

S

proof

A106:
for C1, C2 being Chain of ((k + 1) + 1),G st C1 c= {A} ` & C2 c= {A} ` & S
let A9 be Cell of ((k + 1) + 1),G; :: thesis: ( A9 in {A} ` implies S_{1}[{A9}] )

assume A9 in {A} ` ; :: thesis: S_{1}[{A9}]

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;

end;assume A9 in {A} ` ; :: thesis: S

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

end;

( 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: S_{1}[{A9}]

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

then
for i being Element of Seg d holds l9 . i <= r9 . i
;

hence S_{1}[{A9}]
by A4, A104; :: thesis: verum

end;hence S

S

S

hence del (del {A}) = 0_ (k,G) by A100, Th59; :: thesis: verum

S

A108: for C1, C2 being Chain of ((k + 1) + 1),G st C1 c= C & C2 c= C & S

S

thus S