let d be non zero Nat; for l, r being Element of REAL d
for G being Grating of d st cell (l,r) is Cell of d,G holds
( cell (l,r) = infinite-cell G iff 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 st cell (l,r) is Cell of d,G holds
( cell (l,r) = infinite-cell G iff for i being Element of Seg d holds r . i < l . i )
let G be Grating of d; ( cell (l,r) is Cell of d,G implies ( cell (l,r) = infinite-cell G iff for i being Element of Seg d holds r . i < l . i ) )
assume A1:
cell (l,r) is Cell of d,G
; ( cell (l,r) = infinite-cell G iff for i being Element of Seg d holds r . i < l . i )
then reconsider A = cell (l,r) as Cell of d,G ;
hereby ( ( for i being Element of Seg d holds r . i < l . i ) implies cell (l,r) = infinite-cell G )
assume
cell (
l,
r)
= infinite-cell G
;
for i being Element of Seg d holds r . i < l . ithen consider l9,
r9 being
Element of
REAL d such that A2:
cell (
l,
r)
= cell (
l9,
r9)
and A3:
for
i being
Element of
Seg d holds
(
r9 . i < l9 . i &
[(l9 . i),(r9 . i)] is
Gap of
G . i )
by Def10;
A4:
l = l9
by A2, A3, Th28;
r = r9
by A2, A3, Th28;
hence
for
i being
Element of
Seg d holds
r . i < l . i
by A3, A4;
verum
end;
set i0 = the Element of Seg d;
assume
for i being Element of Seg d holds r . i < l . i
; cell (l,r) = infinite-cell G
then A5:
r . the Element of Seg d < l . the Element of Seg d
;
A6:
A = cell (l,r)
;
for i being Element of Seg d holds
( r . i < l . i & [(l . i),(r . i)] is Gap of G . i )
by A1, A5, Th31;
hence
cell (l,r) = infinite-cell G
by A6, Def10; verum