let d be non zero Nat; :: thesis: 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; :: thesis: 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); :: thesis: ( 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 ) ) )

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 ) ; :: thesis: A in cells (d,G)

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; :: thesis: 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); :: thesis: ( 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 :: thesis: ( 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) )

given l, r being Element of REAL d such that A5:
A = cell (l,r)
and ( 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)
; :: thesis: 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 ) ) :: thesis: verum

end;( 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 ) ) :: thesis: verum

proof

take
l
; :: thesis: ex 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 ) )

take r ; :: thesis: ( 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 ) )

end;( 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 ) )

take r ; :: thesis: ( 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 ) )

per cases
( 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 for i being Element of Seg d holds

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

end;

( 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 for i being Element of Seg d holds

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

suppose
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 ) ) ) ) ; :: thesis: ( 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 ) )

( 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 ) ) ) ) ; :: thesis: ( 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 X being Subset of (Seg d) such that

A3: card X = d 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 ) ) ;

card X = card (Seg d) by A3, FINSEQ_1:57;

then not X c< Seg d by CARD_2:48;

then X = Seg d by XBOOLE_0:def 8;

hence ( 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 ) ) by A1, A4; :: thesis: verum

end;A3: card X = d 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 ) ) ;

card X = card (Seg d) by A3, FINSEQ_1:57;

then not X c< Seg d by CARD_2:48;

then X = Seg d by XBOOLE_0:def 8;

hence ( 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 ) ) by A1, A4; :: thesis: verum

suppose
for i being Element of Seg d holds

( r . i < l . i & [(l . i),(r . i)] is Gap of G . i ) ; :: thesis: ( 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 ) )

( r . i < l . i & [(l . i),(r . i)] is Gap of G . i ) ; :: thesis: ( 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 ) )

hence
( 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 ) )
by A1; :: thesis: verum

end;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 ) ; :: thesis: A in cells (d,G)

per cases
( 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 )
by A7;

end;

suppose A8:
for i being Element of Seg d holds l . i < r . i
; :: thesis: A in cells (d,G)

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 ) ) ) )

end;( 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 ) ) ) )

proof

hence
A in cells (d,G)
by A5, Th29; :: thesis: verum
Seg d c= Seg d
;

then reconsider X = Seg d as Subset of (Seg d) ;

take X ; :: thesis: ( 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 ) ) ) )

thus card X = d by FINSEQ_1:57; :: thesis: 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 ) )

thus 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 A6, A8; :: thesis: verum

end;then reconsider X = Seg d as Subset of (Seg d) ;

take X ; :: thesis: ( 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 ) ) ) )

thus card X = d by FINSEQ_1:57; :: thesis: 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 ) )

thus 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 A6, A8; :: thesis: verum