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

for G being Grating of d st cell (l,r) is Cell of d,G holds

( cell (l,r) = infinite-cell G iff 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 st cell (l,r) is Cell of d,G holds

( cell (l,r) = infinite-cell G iff for i being Element of Seg d holds r . i < l . i )

let G be Grating of d; :: thesis: ( cell (l,r) is Cell of d,G implies ( cell (l,r) = infinite-cell G iff for i being Element of Seg d holds r . i < l . i ) )

assume A1: cell (l,r) is Cell of d,G ; :: thesis: ( cell (l,r) = infinite-cell G iff for i being Element of Seg d holds r . i < l . i )

then reconsider A = cell (l,r) as Cell of d,G ;

assume for i being Element of Seg d holds r . i < l . i ; :: thesis: cell (l,r) = infinite-cell G

then A5: r . the Element of Seg d < l . the Element of Seg d ;

A6: A = cell (l,r) ;

for i being Element of Seg d holds

( r . i < l . i & [(l . i),(r . i)] is Gap of G . i ) by A1, A5, Th31;

hence cell (l,r) = infinite-cell G by A6, Def10; :: thesis: verum

for G being Grating of d st cell (l,r) is Cell of d,G holds

( cell (l,r) = infinite-cell G iff 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 st cell (l,r) is Cell of d,G holds

( cell (l,r) = infinite-cell G iff for i being Element of Seg d holds r . i < l . i )

let G be Grating of d; :: thesis: ( cell (l,r) is Cell of d,G implies ( cell (l,r) = infinite-cell G iff for i being Element of Seg d holds r . i < l . i ) )

assume A1: cell (l,r) is Cell of d,G ; :: thesis: ( cell (l,r) = infinite-cell G iff for i being Element of Seg d holds r . i < l . i )

then reconsider A = cell (l,r) as Cell of d,G ;

hereby :: thesis: ( ( for i being Element of Seg d holds r . i < l . i ) implies cell (l,r) = infinite-cell G )

set i0 = the Element of Seg d;assume
cell (l,r) = infinite-cell G
; :: thesis: for i being Element of Seg d holds r . i < l . i

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

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

A3: for i being Element of Seg d holds

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

A4: l = l9 by A2, A3, Th28;

r = r9 by A2, A3, Th28;

hence for i being Element of Seg d holds r . i < l . i by A3, A4; :: thesis: verum

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

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

A3: for i being Element of Seg d holds

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

A4: l = l9 by A2, A3, Th28;

r = r9 by A2, A3, Th28;

hence for i being Element of Seg d holds r . i < l . i by A3, A4; :: thesis: verum

assume for i being Element of Seg d holds r . i < l . i ; :: thesis: cell (l,r) = infinite-cell G

then A5: r . the Element of Seg d < l . the Element of Seg d ;

A6: A = cell (l,r) ;

for i being Element of Seg d holds

( r . i < l . i & [(l . i),(r . i)] is Gap of G . i ) by A1, A5, Th31;

hence cell (l,r) = infinite-cell G by A6, Def10; :: thesis: verum