let d be non zero Nat; :: thesis: for G being Grating of d

for A being Subset of (REAL d) holds

( A in cells (0,G) iff ex x being Element of REAL d st

( A = cell (x,x) & ( for i being Element of Seg d holds x . i in G . i ) ) )

let G be Grating of d; :: thesis: for A being Subset of (REAL d) holds

( A in cells (0,G) iff ex x being Element of REAL d st

( A = cell (x,x) & ( for i being Element of Seg d holds x . i in G . i ) ) )

let A be Subset of (REAL d); :: thesis: ( A in cells (0,G) iff ex x being Element of REAL d st

( A = cell (x,x) & ( for i being Element of Seg d holds x . i in G . i ) ) )

A7: for i being Element of Seg d holds x . i in G . i ; :: thesis: A in cells (0,G)

ex X being Subset of (Seg d) st

( card X = 0 & ( for i being Element of Seg d holds

( ( i in X & x . i < x . i & [(x . i),(x . i)] is Gap of G . i ) or ( not i in X & x . i = x . i & x . i in G . i ) ) ) )

for A being Subset of (REAL d) holds

( A in cells (0,G) iff ex x being Element of REAL d st

( A = cell (x,x) & ( for i being Element of Seg d holds x . i in G . i ) ) )

let G be Grating of d; :: thesis: for A being Subset of (REAL d) holds

( A in cells (0,G) iff ex x being Element of REAL d st

( A = cell (x,x) & ( for i being Element of Seg d holds x . i in G . i ) ) )

let A be Subset of (REAL d); :: thesis: ( A in cells (0,G) iff ex x being Element of REAL d st

( A = cell (x,x) & ( for i being Element of Seg d holds x . i in G . i ) ) )

hereby :: thesis: ( ex x being Element of REAL d st

( A = cell (x,x) & ( for i being Element of Seg d holds x . i in G . i ) ) implies A in cells (0,G) )

given x being Element of REAL d such that A6:
A = cell (x,x)
and ( A = cell (x,x) & ( for i being Element of Seg d holds x . i in G . i ) ) implies A in cells (0,G) )

assume
A in cells (0,G)
; :: thesis: ex x being Element of REAL d st

( A = cell (x,x) & ( for i being Element of Seg d holds x . i in G . 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 = 0 & ( 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 ( 0 = d & ( for i being Element of Seg d holds

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

consider X being Subset of (Seg d) such that

A3: card X = 0 and

A4: 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 ) ) by A2;

reconsider l9 = l, r9 = r as Function of (Seg d),REAL by Def3;

X = {} by A3;

then A5: for i being Element of Seg d holds

( l9 . i = r9 . i & l . i in G . i ) by A4;

then l9 = r9 by FUNCT_2:63;

hence ex x being Element of REAL d st

( A = cell (x,x) & ( for i being Element of Seg d holds x . i in G . i ) ) by A1, A5; :: thesis: verum

end;( A = cell (x,x) & ( for i being Element of Seg d holds x . i in G . 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 = 0 & ( 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 ( 0 = d & ( for i being Element of Seg d holds

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

consider X being Subset of (Seg d) such that

A3: card X = 0 and

A4: 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 ) ) by A2;

reconsider l9 = l, r9 = r as Function of (Seg d),REAL by Def3;

X = {} by A3;

then A5: for i being Element of Seg d holds

( l9 . i = r9 . i & l . i in G . i ) by A4;

then l9 = r9 by FUNCT_2:63;

hence ex x being Element of REAL d st

( A = cell (x,x) & ( for i being Element of Seg d holds x . i in G . i ) ) by A1, A5; :: thesis: verum

A7: for i being Element of Seg d holds x . i in G . i ; :: thesis: A in cells (0,G)

ex X being Subset of (Seg d) st

( card X = 0 & ( for i being Element of Seg d holds

( ( i in X & x . i < x . i & [(x . i),(x . i)] is Gap of G . i ) or ( not i in X & x . i = x . i & x . i in G . i ) ) ) )

proof

hence
A in cells (0,G)
by A6, Th29; :: thesis: verum
reconsider X = {} as Subset of (Seg d) by XBOOLE_1:2;

take X ; :: thesis: ( card X = 0 & ( for i being Element of Seg d holds

( ( i in X & x . i < x . i & [(x . i),(x . i)] is Gap of G . i ) or ( not i in X & x . i = x . i & x . i in G . i ) ) ) )

thus ( card X = 0 & ( for i being Element of Seg d holds

( ( i in X & x . i < x . i & [(x . i),(x . i)] is Gap of G . i ) or ( not i in X & x . i = x . i & x . i in G . i ) ) ) ) by A7; :: thesis: verum

end;take X ; :: thesis: ( card X = 0 & ( for i being Element of Seg d holds

( ( i in X & x . i < x . i & [(x . i),(x . i)] is Gap of G . i ) or ( not i in X & x . i = x . i & x . i in G . i ) ) ) )

thus ( card X = 0 & ( for i being Element of Seg d holds

( ( i in X & x . i < x . i & [(x . i),(x . i)] is Gap of G . i ) or ( not i in X & x . i = x . i & x . i in G . i ) ) ) ) by A7; :: thesis: verum