let d be non zero Nat; 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; 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; ( cell (l,r) in cells (0,G) iff ( l = r & ( for i being Element of Seg d holds l . i in G . i ) ) )
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 Th34; verum