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

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 )

assume 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 l', r' being Element of REAL d such that
A1: cell l,r = cell l',r' and
A2: for i being Element of Seg d holds [(l' . i),(r' . i)] is Gap of G . i and
A3: ( 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 Th40;
A4: ( 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 A3;
then A5: l = l' by A1, Th32;
r = r' by A1, A4, Th32;
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;

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 Th40; :: thesis: verum