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

for G being Grating of d holds

( cell (l,r) in cells (d,G) iff ( ( for i being Element of Seg d holds [(l . i),(r . i)] is Gap of G . i ) & ( for i being Element of Seg d holds l . i < r . i or for i being Element of Seg d holds r . i < l . i ) ) )

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

( cell (l,r) in cells (d,G) iff ( ( for i being Element of Seg d holds [(l . i),(r . i)] is Gap of G . i ) & ( for i being Element of Seg d holds l . i < r . i or for i being Element of Seg d holds r . i < l . i ) ) )

let G be Grating of d; :: thesis: ( cell (l,r) in cells (d,G) iff ( ( for i being Element of Seg d holds [(l . i),(r . i)] is Gap of G . i ) & ( for i being Element of Seg d holds l . i < r . i or for i being Element of Seg d holds r . i < l . i ) ) )

for G being Grating of d holds

( cell (l,r) in cells (d,G) iff ( ( for i being Element of Seg d holds [(l . i),(r . i)] is Gap of G . i ) & ( for i being Element of Seg d holds l . i < r . i or for i being Element of Seg d holds r . i < l . i ) ) )

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

( cell (l,r) in cells (d,G) iff ( ( for i being Element of Seg d holds [(l . i),(r . i)] is Gap of G . i ) & ( for i being Element of Seg d holds l . i < r . i or for i being Element of Seg d holds r . i < l . i ) ) )

let G be Grating of d; :: thesis: ( cell (l,r) in cells (d,G) iff ( ( for i being Element of Seg d holds [(l . i),(r . i)] is Gap of G . i ) & ( for i being Element of Seg d holds l . i < r . i or for i being Element of Seg d holds r . i < l . i ) ) )

hereby :: thesis: ( ( for i being Element of Seg d holds [(l . i),(r . i)] is Gap of G . i ) & ( for i being Element of Seg d holds l . i < r . i or for i being Element of Seg d holds r . i < l . i ) implies cell (l,r) in cells (d,G) )

thus
( ( for i being Element of Seg d holds [(l . i),(r . i)] is Gap of G . i ) & ( for i being Element of Seg d holds l . i < r . i or for i being Element of Seg d holds r . i < l . i ) implies cell (l,r) in cells (d,G) )
by Th36; :: thesis: verumassume
cell (l,r) in cells (d,G)
; :: thesis: ( ( for i being Element of Seg d holds [(l . i),(r . i)] is Gap of G . i ) & ( for i being Element of Seg d holds l . i < r . i or for i being Element of Seg d holds r . i < l . i ) )

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

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

A2: for i being Element of Seg d holds [(l9 . i),(r9 . i)] is Gap of G . i and

A3: ( for i being Element of Seg d holds l9 . i < r9 . i or for i being Element of Seg d holds r9 . i < l9 . i ) by Th36;

A4: ( for i being Element of Seg d holds l9 . i <= r9 . i or for i being Element of Seg d holds r9 . i < l9 . i ) by A3;

then A5: l = l9 by A1, Th28;

r = r9 by A1, A4, Th28;

hence ( ( for i being Element of Seg d holds [(l . i),(r . i)] is Gap of G . i ) & ( for i being Element of Seg d holds l . i < r . i or for i being Element of Seg d holds r . i < l . i ) ) by A2, A3, A5; :: thesis: verum

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

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

A2: for i being Element of Seg d holds [(l9 . i),(r9 . i)] is Gap of G . i and

A3: ( for i being Element of Seg d holds l9 . i < r9 . i or for i being Element of Seg d holds r9 . i < l9 . i ) by Th36;

A4: ( for i being Element of Seg d holds l9 . i <= r9 . i or for i being Element of Seg d holds r9 . i < l9 . i ) by A3;

then A5: l = l9 by A1, Th28;

r = r9 by A1, A4, Th28;

hence ( ( for i being Element of Seg d holds [(l . i),(r . i)] is Gap of G . i ) & ( for i being Element of Seg d holds l . i < r . i or for i being Element of Seg d holds r . i < l . i ) ) by A2, A3, A5; :: thesis: verum