let d be non zero Element of NAT ; :: thesis:
let G be Grating of d; :: thesis:
A1: d >= 1 by Def2;
let A be Subset of (REAL d); :: thesis:

hereby :: thesis:

assume A in cells 1,G ; :: thesis:
then consider l, r being Element of REAL d such that
A2: ( A = cell l,r & ( 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 A1, Th33;
take l = l; :: thesis:
take r = r; :: thesis:
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:

proof

per cases by A2;

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:

then consider X being Subset of (Seg d) such that
A3: ( 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 ) ) ) ) ;
consider i0 being set such that
A4: X = {i0} by A3, CARD_2:60;
A5: i0 in X by A4, TARSKI:def 1;
then reconsider i0 = i0 as Element of Seg d ;
take i0 ; :: thesis:
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, A3, A5; :: thesis:
let i be Element of Seg d; :: thesis:
( not i in X iff i <> i0 ) by A4, TARSKI:def 1;
hence ( i <> i0 implies ( l . i = r . i & l . i in G . i ) ) by A3; :: thesis:

end;

suppose A6: ( d = 1 & ( for i being Element of Seg d holds
( r . i < l . i & [(l . i),(r . i)] is Gap of G . i ) ) ) ; :: thesis:

reconsider i0 = 1 as Element of Seg d by A1, FINSEQ_1:3;
take i0 ; :: thesis:
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, A6; :: thesis:
let i be Element of Seg d; :: thesis:
( 1 <= i & i <= d ) by FINSEQ_1:3;
hence ( i <> i0 implies ( l . i = r . i & l . i in G . i ) ) by A6, XXREAL_0:1; :: thesis:

end;

given l, r being Element of REAL d, i0 being Element of Seg d such that A7: ( 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:
set X = {i0};

per cases by A7;

suppose A8: l . i0 < r . i0 ; :: thesis:

A9: card {i0} = 1 by CARD_1:50;

now

let i be Element of Seg d; :: thesis:
( 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 A7, A8; :: thesis:

end;

hence A in cells 1,G by A1, A7, A9, Th33; :: thesis:

end;

suppose A10: ( d = 1 & r . i0 < l . i0 ) ; :: thesis:

now

let i be Element of Seg d; :: thesis:
( 1 <= i & i <= d & 1 <= i0 & i0 <= d ) by FINSEQ_1:3;
then ( i = 1 & i0 = 1 ) by A10, XXREAL_0:1;
hence ( r . i < l . i & [(l . i),(r . i)] is Gap of G . i ) by A7, A10; :: thesis:

end;

hence A in cells 1,G by A7, Th33; :: thesis:

end;