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

for l, r being Element of REAL d

for G being Grating of d st d = d9 + 1 holds

( cell (l,r) in cells (d9,G) iff ex i0 being Element of Seg d st

( l . i0 = r . i0 & l . i0 in G . i0 & ( for i being Element of Seg d st i <> i0 holds

( l . i < r . 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 d = d9 + 1 holds

( cell (l,r) in cells (d9,G) iff ex i0 being Element of Seg d st

( l . i0 = r . i0 & l . i0 in G . i0 & ( for i being Element of Seg d st i <> i0 holds

( l . i < r . 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 d = d9 + 1 holds

( cell (l,r) in cells (d9,G) iff ex i0 being Element of Seg d st

( l . i0 = r . i0 & l . i0 in G . i0 & ( for i being Element of Seg d st i <> i0 holds

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

let G be Grating of d; :: thesis: ( d = d9 + 1 implies ( cell (l,r) in cells (d9,G) iff ex i0 being Element of Seg d st

( l . i0 = r . i0 & l . i0 in G . i0 & ( for i being Element of Seg d st i <> i0 holds

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

assume A1: d = d9 + 1 ; :: thesis: ( cell (l,r) in cells (d9,G) iff ex i0 being Element of Seg d st

( l . i0 = r . i0 & l . i0 in G . i0 & ( for i being Element of Seg d st i <> i0 holds

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

( l . i0 = r . i0 & l . i0 in G . i0 & ( for i being Element of Seg d st i <> i0 holds

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

for l, r being Element of REAL d

for G being Grating of d st d = d9 + 1 holds

( cell (l,r) in cells (d9,G) iff ex i0 being Element of Seg d st

( l . i0 = r . i0 & l . i0 in G . i0 & ( for i being Element of Seg d st i <> i0 holds

( l . i < r . 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 d = d9 + 1 holds

( cell (l,r) in cells (d9,G) iff ex i0 being Element of Seg d st

( l . i0 = r . i0 & l . i0 in G . i0 & ( for i being Element of Seg d st i <> i0 holds

( l . i < r . 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 d = d9 + 1 holds

( cell (l,r) in cells (d9,G) iff ex i0 being Element of Seg d st

( l . i0 = r . i0 & l . i0 in G . i0 & ( for i being Element of Seg d st i <> i0 holds

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

let G be Grating of d; :: thesis: ( d = d9 + 1 implies ( cell (l,r) in cells (d9,G) iff ex i0 being Element of Seg d st

( l . i0 = r . i0 & l . i0 in G . i0 & ( for i being Element of Seg d st i <> i0 holds

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

assume A1: d = d9 + 1 ; :: thesis: ( cell (l,r) in cells (d9,G) iff ex i0 being Element of Seg d st

( l . i0 = r . i0 & l . i0 in G . i0 & ( for i being Element of Seg d st i <> i0 holds

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

hereby :: thesis: ( ex i0 being Element of Seg d st

( l . i0 = r . i0 & l . i0 in G . i0 & ( for i being Element of Seg d st i <> i0 holds

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

thus
( ex i0 being Element of Seg d st ( l . i0 = r . i0 & l . i0 in G . i0 & ( for i being Element of Seg d st i <> i0 holds

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

assume
cell (l,r) in cells (d9,G)
; :: thesis: ex i0 being Element of Seg d st

( l . i0 = r . i0 & l . i0 in G . i0 & ( for i being Element of Seg d st i <> i0 holds

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

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

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

A3: l9 . i0 = r9 . i0 and

A4: l9 . i0 in G . i0 and

A5: for i being Element of Seg d st i <> i0 holds

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

take i0 = i0; :: thesis: ( l . i0 = r . i0 & l . i0 in G . i0 & ( for i being Element of Seg d st i <> i0 holds

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

r = r9 by A2, A6, Th28;

hence ( l . i0 = r . i0 & l . i0 in G . i0 & ( for i being Element of Seg d st i <> i0 holds

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

end;( l . i0 = r . i0 & l . i0 in G . i0 & ( for i being Element of Seg d st i <> i0 holds

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

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

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

A3: l9 . i0 = r9 . i0 and

A4: l9 . i0 in G . i0 and

A5: for i being Element of Seg d st i <> i0 holds

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

take i0 = i0; :: thesis: ( l . i0 = r . i0 & l . i0 in G . i0 & ( for i being Element of Seg d st i <> i0 holds

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

A6: now :: thesis: for i being Element of Seg d holds l9 . i <= r9 . i

then A7:
l = l9
by A2, Th28;let i be Element of Seg d; :: thesis: l9 . i <= r9 . i

( i = i0 or i <> i0 ) ;

hence l9 . i <= r9 . i by A3, A5; :: thesis: verum

end;( i = i0 or i <> i0 ) ;

hence l9 . i <= r9 . i by A3, A5; :: thesis: verum

r = r9 by A2, A6, Th28;

hence ( l . i0 = r . i0 & l . i0 in G . i0 & ( for i being Element of Seg d st i <> i0 holds

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

( l . i0 = r . i0 & l . i0 in G . i0 & ( for i being Element of Seg d st i <> i0 holds

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