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) = infinite-cell G iff 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 holds
( cell (l,r) = infinite-cell G iff 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: ( cell (l,r) = infinite-cell G iff for i being Element of Seg d holds
( r . i < l . i & [(l . i),(r . i)] is Gap of G . i ) )

hereby :: thesis: ( ( 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) = infinite-cell G )

assume cell (l,r) = infinite-cell G ; :: thesis: 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
A1: cell (l,r) = cell (l9,r9) and
A2: for i being Element of Seg d holds
( r9 . i < l9 . i & [(l9 . i),(r9 . i)] is Gap of G . i ) by Def10;
A3: l = l9 by A1, A2, Th28;
r = r9 by A1, A2, Th28;
hence for i being Element of Seg d holds
( r . i < l . i & [(l . i),(r . i)] is Gap of G . i ) by A2, A3; :: thesis: verum

end;

assume A4: for i being Element of Seg d holds
( r . i < l . i & [(l . i),(r . i)] is Gap of G . i ) ; :: thesis: cell (l,r) = infinite-cell G
then cell (l,r) is Cell of d,G by Th30;
hence cell (l,r) = infinite-cell G by A4, Def10; :: thesis: verum