let k be Nat; :: thesis: for d being non zero Nat

for G being Grating of d st k <= d holds

for A being Subset of (REAL d) holds

( A in cells (k,G) iff ex l, r being Element of REAL d st

( A = cell (l,r) & ( ex X being Subset of (Seg d) st

( card X = k & ( 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 ( k = d & ( for i being Element of Seg d holds

( r . i < l . i & [(l . i),(r . i)] is Gap of G . i ) ) ) ) ) )

let d be non zero Nat; :: thesis: for G being Grating of d st k <= d holds

for A being Subset of (REAL d) holds

( A in cells (k,G) iff ex l, r being Element of REAL d st

( A = cell (l,r) & ( ex X being Subset of (Seg d) st

( card X = k & ( 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 ( k = d & ( 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; :: thesis: ( k <= d implies for A being Subset of (REAL d) holds

( A in cells (k,G) iff ex l, r being Element of REAL d st

( A = cell (l,r) & ( ex X being Subset of (Seg d) st

( card X = k & ( 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 ( k = d & ( for i being Element of Seg d holds

( r . i < l . i & [(l . i),(r . i)] is Gap of G . i ) ) ) ) ) ) )

assume k <= d ; :: thesis: for A being Subset of (REAL d) holds

( A in cells (k,G) iff ex l, r being Element of REAL d st

( A = cell (l,r) & ( ex X being Subset of (Seg d) st

( card X = k & ( 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 ( k = d & ( for i being Element of Seg d holds

( r . i < l . i & [(l . i),(r . i)] is Gap of G . i ) ) ) ) ) )

then cells (k,G) = { (cell (l,r)) where l, r is Element of REAL d : ( ex X being Subset of (Seg d) st

( card X = k & ( 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 ( k = d & ( for i being Element of Seg d holds

( r . i < l . i & [(l . i),(r . i)] is Gap of G . i ) ) ) ) } by Def7;

hence for A being Subset of (REAL d) holds

( A in cells (k,G) iff ex l, r being Element of REAL d st

( A = cell (l,r) & ( ex X being Subset of (Seg d) st

( card X = k & ( 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 ( k = d & ( for i being Element of Seg d holds

( r . i < l . i & [(l . i),(r . i)] is Gap of G . i ) ) ) ) ) ) ; :: thesis: verum

for G being Grating of d st k <= d holds

for A being Subset of (REAL d) holds

( A in cells (k,G) iff ex l, r being Element of REAL d st

( A = cell (l,r) & ( ex X being Subset of (Seg d) st

( card X = k & ( 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 ( k = d & ( for i being Element of Seg d holds

( r . i < l . i & [(l . i),(r . i)] is Gap of G . i ) ) ) ) ) )

let d be non zero Nat; :: thesis: for G being Grating of d st k <= d holds

for A being Subset of (REAL d) holds

( A in cells (k,G) iff ex l, r being Element of REAL d st

( A = cell (l,r) & ( ex X being Subset of (Seg d) st

( card X = k & ( 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 ( k = d & ( 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; :: thesis: ( k <= d implies for A being Subset of (REAL d) holds

( A in cells (k,G) iff ex l, r being Element of REAL d st

( A = cell (l,r) & ( ex X being Subset of (Seg d) st

( card X = k & ( 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 ( k = d & ( for i being Element of Seg d holds

( r . i < l . i & [(l . i),(r . i)] is Gap of G . i ) ) ) ) ) ) )

assume k <= d ; :: thesis: for A being Subset of (REAL d) holds

( A in cells (k,G) iff ex l, r being Element of REAL d st

( A = cell (l,r) & ( ex X being Subset of (Seg d) st

( card X = k & ( 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 ( k = d & ( for i being Element of Seg d holds

( r . i < l . i & [(l . i),(r . i)] is Gap of G . i ) ) ) ) ) )

then cells (k,G) = { (cell (l,r)) where l, r is Element of REAL d : ( ex X being Subset of (Seg d) st

( card X = k & ( 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 ( k = d & ( for i being Element of Seg d holds

( r . i < l . i & [(l . i),(r . i)] is Gap of G . i ) ) ) ) } by Def7;

hence for A being Subset of (REAL d) holds

( A in cells (k,G) iff ex l, r being Element of REAL d st

( A = cell (l,r) & ( ex X being Subset of (Seg d) st

( card X = k & ( 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 ( k = d & ( for i being Element of Seg d holds

( r . i < l . i & [(l . i),(r . i)] is Gap of G . i ) ) ) ) ) ) ; :: thesis: verum