let k be Nat; :: thesis: for d being non zero Nat

for l, r being Element of REAL d

for G being Grating of d st k <= d holds

( cell (l,r) in cells (k,G) iff ( ex X being Subset of (Seg d) st

( card X = k & ( 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 = d & ( for i being Element of Seg d holds

( r . i < l . i & [(l . i),(r . i)] is Gap of G . i ) ) ) ) )

let d be non zero Nat; :: thesis: for l, r being Element of REAL d

for G being Grating of d st k <= d holds

( cell (l,r) in cells (k,G) iff ( ex X being Subset of (Seg d) st

( card X = k & ( 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 = d & ( for i being Element of Seg d holds

( r . i < l . i & [(l . i),(r . i)] is Gap of G . i ) ) ) ) )

let l, r be Element of REAL d; :: thesis: for G being Grating of d st k <= d holds

( cell (l,r) in cells (k,G) iff ( ex X being Subset of (Seg d) st

( card X = k & ( 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 = d & ( for i being Element of Seg d holds

( r . i < l . i & [(l . i),(r . i)] is Gap of G . i ) ) ) ) )

let G be Grating of d; :: thesis: ( k <= d implies ( cell (l,r) in cells (k,G) iff ( ex X being Subset of (Seg d) st

( card X = k & ( 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 = d & ( for i being Element of Seg d holds

( r . i < l . i & [(l . i),(r . i)] is Gap of G . i ) ) ) ) ) )

assume A1: k <= d ; :: thesis: ( cell (l,r) in cells (k,G) iff ( ex X being Subset of (Seg d) st

( card X = k & ( 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 = d & ( for i being Element of Seg d holds

( r . i < l . i & [(l . i),(r . i)] is Gap of G . i ) ) ) ) )

( card X = k & ( 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 = d & ( for i being Element of Seg d holds

( r . i < l . i & [(l . i),(r . i)] is Gap of G . i ) ) ) ) implies cell (l,r) in cells (k,G) ) by A1, Th29; :: thesis: verum

for l, r being Element of REAL d

for G being Grating of d st k <= d holds

( cell (l,r) in cells (k,G) iff ( ex X being Subset of (Seg d) st

( card X = k & ( 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 = d & ( for i being Element of Seg d holds

( r . i < l . i & [(l . i),(r . i)] is Gap of G . i ) ) ) ) )

let d be non zero Nat; :: thesis: for l, r being Element of REAL d

for G being Grating of d st k <= d holds

( cell (l,r) in cells (k,G) iff ( ex X being Subset of (Seg d) st

( card X = k & ( 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 = d & ( for i being Element of Seg d holds

( r . i < l . i & [(l . i),(r . i)] is Gap of G . i ) ) ) ) )

let l, r be Element of REAL d; :: thesis: for G being Grating of d st k <= d holds

( cell (l,r) in cells (k,G) iff ( ex X being Subset of (Seg d) st

( card X = k & ( 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 = d & ( for i being Element of Seg d holds

( r . i < l . i & [(l . i),(r . i)] is Gap of G . i ) ) ) ) )

let G be Grating of d; :: thesis: ( k <= d implies ( cell (l,r) in cells (k,G) iff ( ex X being Subset of (Seg d) st

( card X = k & ( 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 = d & ( for i being Element of Seg d holds

( r . i < l . i & [(l . i),(r . i)] is Gap of G . i ) ) ) ) ) )

assume A1: k <= d ; :: thesis: ( cell (l,r) in cells (k,G) iff ( ex X being Subset of (Seg d) st

( card X = k & ( 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 = d & ( for i being Element of Seg d holds

( r . i < l . i & [(l . i),(r . i)] is Gap of G . i ) ) ) ) )

hereby :: thesis: ( ( ex X being Subset of (Seg d) st

( card X = k & ( 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 = d & ( for i being Element of Seg d holds

( r . i < l . i & [(l . i),(r . i)] is Gap of G . i ) ) ) ) implies cell (l,r) in cells (k,G) )

thus
( ( ex X being Subset of (Seg d) st ( card X = k & ( 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 = d & ( for i being Element of Seg d holds

( r . i < l . i & [(l . i),(r . i)] is Gap of G . i ) ) ) ) implies cell (l,r) in cells (k,G) )

assume
cell (l,r) in cells (k,G)
; :: thesis: ( ex X being Subset of (Seg d) st

( card X = k & ( 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 = d & ( for i being Element of Seg d holds

( r . i < l . i & [(l . i),(r . i)] is Gap of G . i ) ) ) )

then consider l9, r9 being Element of REAL d such that

A2: cell (l,r) = cell (l9,r9) and

A3: ( 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 A1, Th29;

( l = l9 & r = r9 )

( card X = k & ( 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 = d & ( for i being Element of Seg d holds

( r . i < l . i & [(l . i),(r . i)] is Gap of G . i ) ) ) ) by A3; :: thesis: verum

end;( card X = k & ( 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 = d & ( for i being Element of Seg d holds

( r . i < l . i & [(l . i),(r . i)] is Gap of G . i ) ) ) )

then consider l9, r9 being Element of REAL d such that

A2: cell (l,r) = cell (l9,r9) and

A3: ( 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 A1, Th29;

( l = l9 & r = r9 )

proof
end;

hence
( ex X being Subset of (Seg d) st per cases
( 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 for i being Element of Seg d holds

( r9 . i < l9 . i & [(l9 . i),(r9 . i)] is Gap of G . i ) ) by A3;

end;

( 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 for i being Element of Seg d holds

( r9 . i < l9 . i & [(l9 . i),(r9 . i)] is Gap of G . i ) ) by A3;

suppose
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 ) ) ) ) ; :: thesis: ( l = l9 & r = r9 )

( 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 ) ) ) ) ; :: thesis: ( l = l9 & r = r9 )

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

hence ( l = l9 & r = r9 ) by A2, Th28; :: thesis: verum

end;hence ( l = l9 & r = r9 ) by A2, Th28; :: thesis: verum

( card X = k & ( 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 = d & ( for i being Element of Seg d holds

( r . i < l . i & [(l . i),(r . i)] is Gap of G . i ) ) ) ) by A3; :: thesis: verum

( card X = k & ( 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 = d & ( for i being Element of Seg d holds

( r . i < l . i & [(l . i),(r . i)] is Gap of G . i ) ) ) ) implies cell (l,r) in cells (k,G) ) by A1, Th29; :: thesis: verum