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 0 ,G iff ( l = r & ( for i being Element of Seg d holds l . i in G . i ) ) )
let l, r be Element of REAL d; :: thesis: for G being Grating of d holds
( cell l,r in cells 0 ,G iff ( l = r & ( for i being Element of Seg d holds l . i in G . i ) ) )
let G be Grating of d; :: thesis: ( cell l,r in cells 0 ,G iff ( l = r & ( for i being Element of Seg d holds l . i in G . i ) ) )

hereby :: thesis: ( l = r & ( for i being Element of Seg d holds l . i in G . i ) implies cell l,r in cells 0 ,G )

assume cell l,r in cells 0 ,G ; :: thesis: ( l = r & ( for i being Element of Seg d holds l . i in G . i ) )
then consider x being Element of REAL d such that
A1: cell l,r = cell x,x and
A2: for i being Element of Seg d holds x . i in G . i by Th38;
A3: for i being Element of Seg d holds x . i <= x . i ;
then l = x by A1, Th32;
hence ( l = r & ( for i being Element of Seg d holds l . i in G . i ) ) by A1, A2, A3, Th32; :: thesis: verum

end;

thus ( l = r & ( for i being Element of Seg d holds l . i in G . i ) implies cell l,r in cells 0 ,G ) by Th38; :: thesis: verum