let d be non zero Element of 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 ;

hereby :: thesis: ( ( for i being Element of Seg d holds r . i < l . 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
then consider l', r' being Element of REAL d such that
A2: ( cell l,r = 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 Def11;
( l = l' & r = r' ) by A2, Th32;
hence for i being Element of Seg d holds r . i < l . i by A2; :: thesis: verum

end;

consider i0 being Element of Seg d;
assume for i being Element of Seg d holds r . i < l . i ; :: thesis: cell l,r = infinite-cell G
then r . i0 < l . i0 ;
then ( 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, Th35;
hence cell l,r = infinite-cell G by Def11; :: thesis: verum