let k be Nat; :: thesis: for d being non zero Nat
for l, r being Element of REAL d
for G being Grating of d st k <= d & cell (l,r) in cells (k,G) holds
for i being Element of Seg d holds
( l . i in G . i & r . i in G . i )
let d be non zero Nat; :: thesis: for l, r being Element of REAL d
for G being Grating of d st k <= d & cell (l,r) in cells (k,G) holds
for i being Element of Seg d holds
( l . i in G . i & r . i in G . i )
let l, r be Element of REAL d; :: thesis: for G being Grating of d st k <= d & cell (l,r) in cells (k,G) holds
for i being Element of Seg d holds
( l . i in G . i & r . i in G . i )
let G be Grating of d; :: thesis: ( k <= d & cell (l,r) in cells (k,G) implies for i being Element of Seg d holds
( l . i in G . i & r . i in G . i ) )
assume that
A1: k <= d and
A2: cell (l,r) in cells (k,G) ; :: thesis: for i being Element of Seg d holds
( l . i in G . i & r . i in G . i )
let i be Element of Seg d; :: thesis: ( l . i in G . i & r . i in G . i )
( ( l . i < r . i & [(l . i),(r . i)] is Gap of G . i ) or ( l . i = r . i & l . i in G . i ) or ( r . i < l . i & [(l . i),(r . i)] is Gap of G . i ) ) by A1, A2, Th31;
hence ( l . i in G . i & r . i in G . i ) by Th13; :: thesis: verum