let d be non zero Nat; :: thesis: for G being Grating of d
for A being Subset of (REAL d) holds
( A in cells (1,G) iff ex l, r being Element of REAL d ex i0 being Element of Seg d st
( A = cell (l,r) & ( l . i0 < r . i0 or ( d = 1 & r . i0 < l . i0 ) ) & [(l . i0),(r . i0)] is Gap of G . i0 & ( for i being Element of Seg d st i <> i0 holds
( l . i = r . i & l . i in G . i ) ) ) )

let G be Grating of d; :: thesis: for A being Subset of (REAL d) holds
( A in cells (1,G) iff ex l, r being Element of REAL d ex i0 being Element of Seg d st
( A = cell (l,r) & ( l . i0 < r . i0 or ( d = 1 & r . i0 < l . i0 ) ) & [(l . i0),(r . i0)] is Gap of G . i0 & ( for i being Element of Seg d st i <> i0 holds
( l . i = r . i & l . i in G . i ) ) ) )

A1: d >= 1 by Def2;
let A be Subset of (REAL d); :: thesis: ( A in cells (1,G) iff ex l, r being Element of REAL d ex i0 being Element of Seg d st
( A = cell (l,r) & ( l . i0 < r . i0 or ( d = 1 & r . i0 < l . i0 ) ) & [(l . i0),(r . i0)] is Gap of G . i0 & ( for i being Element of Seg d st i <> i0 holds
( l . i = r . i & l . i in G . i ) ) ) )

hereby :: thesis: ( ex l, r being Element of REAL d ex i0 being Element of Seg d st
( A = cell (l,r) & ( l . i0 < r . i0 or ( d = 1 & r . i0 < l . i0 ) ) & [(l . i0),(r . i0)] is Gap of G . i0 & ( for i being Element of Seg d st i <> i0 holds
( l . i = r . i & l . i in G . i ) ) ) implies A in cells (1,G) )
assume A in cells (1,G) ; :: thesis: ex l, r being Element of REAL d ex i0 being Element of Seg d st
( A = cell (l,r) & ( l . i0 < r . i0 or ( d = 1 & r . i0 < l . i0 ) ) & [(l . i0),(r . i0)] is Gap of G . i0 & ( for i being Element of Seg d st i <> i0 holds
( l . i = r . i & l . i in G . i ) ) )

then consider l, r being Element of REAL d such that
A2: A = cell (l,r) and
A3: ( ex X being Subset of (Seg d) st
( card X = 1 & ( 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 ( 1 = d & ( for i being Element of Seg d holds
( r . i < l . i & [(l . i),(r . i)] is Gap of G . i ) ) ) ) by ;
take l = l; :: thesis: ex r being Element of REAL d ex i0 being Element of Seg d st
( A = cell (l,r) & ( l . i0 < r . i0 or ( d = 1 & r . i0 < l . i0 ) ) & [(l . i0),(r . i0)] is Gap of G . i0 & ( for i being Element of Seg d st i <> i0 holds
( l . i = r . i & l . i in G . i ) ) )

take r = r; :: thesis: ex i0 being Element of Seg d st
( A = cell (l,r) & ( l . i0 < r . i0 or ( d = 1 & r . i0 < l . i0 ) ) & [(l . i0),(r . i0)] is Gap of G . i0 & ( for i being Element of Seg d st i <> i0 holds
( l . i = r . i & l . i in G . i ) ) )

thus ex i0 being Element of Seg d st
( A = cell (l,r) & ( l . i0 < r . i0 or ( d = 1 & r . i0 < l . i0 ) ) & [(l . i0),(r . i0)] is Gap of G . i0 & ( for i being Element of Seg d st i <> i0 holds
( l . i = r . i & l . i in G . i ) ) ) :: thesis: verum
proof
per cases ( ex X being Subset of (Seg d) st
( card X = 1 & ( 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 = 1 & ( for i being Element of Seg d holds
( r . i < l . i & [(l . i),(r . i)] is Gap of G . i ) ) ) )
by A3;
suppose ex X being Subset of (Seg d) st
( card X = 1 & ( 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: ex i0 being Element of Seg d st
( A = cell (l,r) & ( l . i0 < r . i0 or ( d = 1 & r . i0 < l . i0 ) ) & [(l . i0),(r . i0)] is Gap of G . i0 & ( for i being Element of Seg d st i <> i0 holds
( l . i = r . i & l . i in G . i ) ) )

then consider X being Subset of (Seg d) such that
A4: card X = 1 and
A5: 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 ) ) ;
consider i0 being object such that
A6: X = {i0} by ;
A7: i0 in X by ;
then reconsider i0 = i0 as Element of Seg d ;
take i0 ; :: thesis: ( A = cell (l,r) & ( l . i0 < r . i0 or ( d = 1 & r . i0 < l . i0 ) ) & [(l . i0),(r . i0)] is Gap of G . i0 & ( for i being Element of Seg d st i <> i0 holds
( l . i = r . i & l . i in G . i ) ) )

thus ( A = cell (l,r) & ( l . i0 < r . i0 or ( d = 1 & r . i0 < l . i0 ) ) & [(l . i0),(r . i0)] is Gap of G . i0 ) by A2, A5, A7; :: thesis: for i being Element of Seg d st i <> i0 holds
( l . i = r . i & l . i in G . i )

let i be Element of Seg d; :: thesis: ( i <> i0 implies ( l . i = r . i & l . i in G . i ) )
( not i in X iff i <> i0 ) by ;
hence ( i <> i0 implies ( l . i = r . i & l . i in G . i ) ) by A5; :: thesis: verum
end;
suppose A8: ( d = 1 & ( for i being Element of Seg d holds
( r . i < l . i & [(l . i),(r . i)] is Gap of G . i ) ) ) ; :: thesis: ex i0 being Element of Seg d st
( A = cell (l,r) & ( l . i0 < r . i0 or ( d = 1 & r . i0 < l . i0 ) ) & [(l . i0),(r . i0)] is Gap of G . i0 & ( for i being Element of Seg d st i <> i0 holds
( l . i = r . i & l . i in G . i ) ) )

reconsider i0 = 1 as Element of Seg d by ;
take i0 ; :: thesis: ( A = cell (l,r) & ( l . i0 < r . i0 or ( d = 1 & r . i0 < l . i0 ) ) & [(l . i0),(r . i0)] is Gap of G . i0 & ( for i being Element of Seg d st i <> i0 holds
( l . i = r . i & l . i in G . i ) ) )

thus ( A = cell (l,r) & ( l . i0 < r . i0 or ( d = 1 & r . i0 < l . i0 ) ) & [(l . i0),(r . i0)] is Gap of G . i0 ) by A2, A8; :: thesis: for i being Element of Seg d st i <> i0 holds
( l . i = r . i & l . i in G . i )

let i be Element of Seg d; :: thesis: ( i <> i0 implies ( l . i = r . i & l . i in G . i ) )
A9: 1 <= i by FINSEQ_1:1;
i <= d by FINSEQ_1:1;
hence ( i <> i0 implies ( l . i = r . i & l . i in G . i ) ) by ; :: thesis: verum
end;
end;
end;
end;
given l, r being Element of REAL d, i0 being Element of Seg d such that A10: A = cell (l,r) and
A11: ( l . i0 < r . i0 or ( d = 1 & r . i0 < l . i0 ) ) and
A12: [(l . i0),(r . i0)] is Gap of G . i0 and
A13: for i being Element of Seg d st i <> i0 holds
( l . i = r . i & l . i in G . i ) ; :: thesis: A in cells (1,G)
set X = {i0};
per cases ( l . i0 < r . i0 or ( d = 1 & r . i0 < l . i0 ) ) by A11;
suppose A14: l . i0 < r . i0 ; :: thesis: A in cells (1,G)
A15: card {i0} = 1 by CARD_1:30;
now :: thesis: for i being Element of Seg d holds
( ( i in {i0} & l . i < r . i & [(l . i),(r . i)] is Gap of G . i ) or ( not i in {i0} & l . i = r . i & l . i in G . i ) )
let i be Element of Seg d; :: thesis: ( ( i in {i0} & l . i < r . i & [(l . i),(r . i)] is Gap of G . i ) or ( not i in {i0} & l . i = r . i & l . i in G . i ) )
( i in {i0} iff i = i0 ) by TARSKI:def 1;
hence ( ( i in {i0} & l . i < r . i & [(l . i),(r . i)] is Gap of G . i ) or ( not i in {i0} & l . i = r . i & l . i in G . i ) ) by ; :: thesis: verum
end;
hence A in cells (1,G) by A1, A10, A15, Th29; :: thesis: verum
end;
suppose A16: ( d = 1 & r . i0 < l . i0 ) ; :: thesis: A in cells (1,G)
now :: thesis: for i being Element of Seg d holds
( r . i < l . i & [(l . i),(r . i)] is Gap of G . i )
let i be Element of Seg d; :: thesis: ( r . i < l . i & [(l . i),(r . i)] is Gap of G . i )
A17: 1 <= i by FINSEQ_1:1;
A18: i <= d by FINSEQ_1:1;
A19: 1 <= i0 by FINSEQ_1:1;
A20: i0 <= d by FINSEQ_1:1;
A21: i = 1 by ;
i0 = 1 by ;
hence ( r . i < l . i & [(l . i),(r . i)] is Gap of G . i ) by ; :: thesis: verum
end;
hence A in cells (1,G) by ; :: thesis: verum
end;
end;