let d be non zero Nat; for G being Grating of d
for A being Subset of (REAL d) holds
( A in cells (d,G) iff ex l, r being Element of REAL d st
( A = cell (l,r) & ( 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; for A being Subset of (REAL d) holds
( A in cells (d,G) iff ex l, r being Element of REAL d st
( A = cell (l,r) & ( 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 A be Subset of (REAL d); ( A in cells (d,G) iff ex l, r being Element of REAL d st
( A = cell (l,r) & ( 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 ( ex l, r being Element of REAL d st
( A = cell (l,r) & ( 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 A in cells (d,G) )
assume
A in cells (
d,
G)
;
ex l, r being Element of REAL d st
( A = cell (l,r) & ( 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 l,
r being
Element of
REAL d such that A1:
A = cell (
l,
r)
and A2:
( ex
X being
Subset of
(Seg d) st
(
card X = d & ( for
i being
Element of
Seg d holds
( (
i in X &
l . i < r . i &
[(l . i),(r . i)] is
Gap of
G . i ) or ( not
i in X &
l . i = r . i &
l . i in G . i ) ) ) ) or (
d = d & ( for
i being
Element of
Seg d holds
(
r . i < l . i &
[(l . i),(r . i)] is
Gap of
G . i ) ) ) )
by Th29;
thus
ex
l,
r being
Element of
REAL d st
(
A = cell (
l,
r) & ( 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 ) )
verum
end;
given l, r being Element of REAL d such that A5:
A = cell (l,r)
and
A6:
for i being Element of Seg d holds [(l . i),(r . i)] is Gap of G . i
and
A7:
( 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 )
; A in cells (d,G)