let d be non zero Element of 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 ) ) )

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 )

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 & ( 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 Th33;
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 ) )

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 A1;

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

then consider X being Subset of (Seg d) such that
A2: ( 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 ) ) ) ) ;
card X = card (Seg d) by A2, FINSEQ_1:78;
then not X c< Seg d by CARD_2:67;
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, A2; :: thesis: verum

end;

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

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;

end;

end;

end;

given l, r being Element of REAL d such that A3: ( 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: 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 A3;

suppose A4: 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 ) ) ) )

proof

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:78; :: 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 A3, A4; :: thesis: verum

end;

hence A in cells d,G by A3, Th33; :: thesis: verum

end;

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

hence A in cells d,G by A3, Th33; :: thesis: verum

end;

end;