theorem Th31: :: CHAIN_1:34

for k being Nat
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) & ex i being Element of Seg d st
( not ( l . i < r . i & [(l . i),(r . i)] is Gap of G . i ) & not ( l . i = r . i & l . i in G . i ) ) holds
for i being Element of Seg d holds
( r . i < l . i & [(l . i),(r . i)] is Gap of G . i )