theorem Th42:
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 <= d &
k9 <= d &
cell (
l,
r)
in cells (
k,
G) &
cell (
l9,
r9)
in cells (
k9,
G) &
cell (
l,
r)
c= cell (
l9,
r9) holds
for
i being
Element of
Seg d holds
( (
l . i = l9 . i &
r . i = r9 . i ) or (
l . i = l9 . i &
r . i = l9 . i ) or (
l . i = r9 . i &
r . i = r9 . i ) or (
l . i <= r . i &
r9 . i < l9 . i &
r9 . i <= l . i &
r . i <= l9 . i ) )