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) 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 ) ) )

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) )

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; :: thesis: verumassume
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 Th34;

A3: for i being Element of Seg d holds x . i <= x . i ;

then l = x by A1, Th28;

hence ( l = r & ( for i being Element of Seg d holds l . i in G . i ) ) by A1, A2, A3, Th28; :: thesis: verum

end;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 Th34;

A3: for i being Element of Seg d holds x . i <= x . i ;

then l = x by A1, Th28;

hence ( l = r & ( for i being Element of Seg d holds l . i in G . i ) ) by A1, A2, A3, Th28; :: thesis: verum