theorem Th43:
for
k,
k9 being
Nat for
d being non
zero Nat for
l,
r,
l9,
r9 being
Element of
REAL d for
G being
Grating of
d st
k < k9 &
k9 <= d &
cell (
l,
r)
in cells (
k,
G) &
cell (
l9,
r9)
in cells (
k9,
G) &
cell (
l,
r)
c= cell (
l9,
r9) holds
ex
i being
Element of
Seg d st
( (
l . i = l9 . i &
r . i = l9 . i ) or (
l . i = r9 . i &
r . i = r9 . i ) )