let d be non zero Nat; for l, r being Element of REAL d
for G being Grating of d holds
( cell (l,r) = infinite-cell G iff for i being Element of Seg d holds
( r . i < l . i & [(l . i),(r . i)] is Gap of G . i ) )
let l, r be Element of REAL d; for G being Grating of d holds
( cell (l,r) = infinite-cell G iff for i being Element of Seg d holds
( r . i < l . i & [(l . i),(r . i)] is Gap of G . i ) )
let G be Grating of d; ( cell (l,r) = infinite-cell G iff for i being Element of Seg d holds
( r . i < l . i & [(l . i),(r . i)] is Gap of G . i ) )
hereby ( ( for i being Element of Seg d holds
( r . i < l . i & [(l . i),(r . i)] is Gap of G . 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 . i & [(l . i),(r . i)] is Gap of G . 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
(
r9 . i < l9 . i &
[(l9 . i),(r9 . i)] is
Gap of
G . i )
by Def10;
A3:
l = l9
by A1, A2, Th28;
r = r9
by A1, A2, Th28;
hence
for
i being
Element of
Seg d holds
(
r . i < l . i &
[(l . i),(r . i)] is
Gap of
G . i )
by A2, A3;
verum
end;
assume A4:
for i being Element of Seg d holds
( r . i < l . i & [(l . i),(r . i)] is Gap of G . i )
; cell (l,r) = infinite-cell G
then
cell (l,r) is Cell of d,G
by Th30;
hence
cell (l,r) = infinite-cell G
by A4, Def10; verum