let d be non zero Nat; for l, r being Element of REAL d
for G being Grating of d holds
( cell (l,r) in cells (d,G) iff ( ( for i being Element of Seg d holds [(l . i),(r . i)] is Gap of G . i ) & ( for i being Element of Seg d holds l . i < r . i or for i being Element of Seg d holds r . i < l . i ) ) )
let l, r be Element of REAL d; for G being Grating of d holds
( cell (l,r) in cells (d,G) iff ( ( for i being Element of Seg d holds [(l . i),(r . i)] is Gap of G . i ) & ( for i being Element of Seg d holds l . i < r . i or for i being Element of Seg d holds r . i < l . i ) ) )
let G be Grating of d; ( cell (l,r) in cells (d,G) iff ( ( for i being Element of Seg d holds [(l . i),(r . i)] is Gap of G . i ) & ( for i being Element of Seg d holds l . i < r . i or for i being Element of Seg d holds r . i < l . i ) ) )
hereby ( ( for i being Element of Seg d holds [(l . i),(r . i)] is Gap of G . i ) & ( for i being Element of Seg d holds l . i < r . i or for i being Element of Seg d holds r . i < l . i ) implies cell (l,r) in cells (d,G) )
assume
cell (
l,
r)
in cells (
d,
G)
;
( ( for i being Element of Seg d holds [(l . i),(r . i)] is Gap of G . i ) & ( for i being Element of Seg d holds l . i < r . i or for i being Element of Seg d holds r . i < l . i ) )then consider l9,
r9 being
Element of
REAL d such that A1:
cell (
l,
r)
= cell (
l9,
r9)
and A2:
for
i being
Element of
Seg d holds
[(l9 . i),(r9 . i)] is
Gap of
G . i
and A3:
( for
i being
Element of
Seg d holds
l9 . i < r9 . i or for
i being
Element of
Seg d holds
r9 . i < l9 . i )
by Th36;
A4:
( for
i being
Element of
Seg d holds
l9 . i <= r9 . i or for
i being
Element of
Seg d holds
r9 . i < l9 . i )
by A3;
then A5:
l = l9
by A1, Th28;
r = r9
by A1, A4, Th28;
hence
( ( for
i being
Element of
Seg d holds
[(l . i),(r . i)] is
Gap of
G . i ) & ( for
i being
Element of
Seg d holds
l . i < r . i or for
i being
Element of
Seg d holds
r . i < l . i ) )
by A2, A3, A5;
verum
end;
thus
( ( for i being Element of Seg d holds [(l . i),(r . i)] is Gap of G . i ) & ( for i being Element of Seg d holds l . i < r . i or for i being Element of Seg d holds r . i < l . i ) implies cell (l,r) in cells (d,G) )
by Th36; verum