let d' be Element of NAT ; :: thesis: for d being non zero Element of NAT
for G being Grating of d st d = d' + 1 holds
for A being Subset of (REAL d) holds
( A in cells d',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 & l . i0 in G . i0 & ( for i being Element of Seg d st i <> i0 holds
( l . i < r . i & [(l . i),(r . i)] is Gap of G . i ) ) ) )
let d be non zero Element of NAT ; :: thesis: for G being Grating of d st d = d' + 1 holds
for A being Subset of (REAL d) holds
( A in cells d',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 & l . i0 in G . i0 & ( for i being Element of Seg d st i <> i0 holds
( l . i < r . i & [(l . i),(r . i)] is Gap of G . i ) ) ) )
let G be Grating of d; :: thesis: ( d = d' + 1 implies for A being Subset of (REAL d) holds
( A in cells d',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 & l . i0 in G . i0 & ( for i being Element of Seg d st i <> i0 holds
( l . i < r . i & [(l . i),(r . i)] is Gap of G . i ) ) ) ) )
assume A1: d = d' + 1 ; :: thesis: for A being Subset of (REAL d) holds
( A in cells d',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 & l . i0 in G . i0 & ( for i being Element of Seg d st i <> i0 holds
( l . i < r . i & [(l . i),(r . i)] is Gap of G . i ) ) ) )
then A2: d' < d by NAT_1:13;
let A be Subset of (REAL d); :: thesis: ( A in cells d',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 & l . i0 in G . i0 & ( for i being Element of Seg d st i <> i0 holds
( l . i < r . i & [(l . i),(r . i)] is Gap of 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 & l . i0 in G . i0 & ( for i being Element of Seg d st i <> i0 holds
( l . i < r . i & [(l . i),(r . i)] is Gap of G . i ) ) ) implies A in cells d',G )

assume A in cells d',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 & l . i0 in G . i0 & ( for i being Element of Seg d st i <> i0 holds
( l . i < r . i & [(l . i),(r . i)] is Gap of G . i ) ) )
then consider l, r being Element of REAL d such that
A3: ( 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 A2, Th33;
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 & l . i0 in G . i0 & ( for i being Element of Seg d st i <> i0 holds
( l . i < r . i & [(l . i),(r . i)] is Gap of G . i ) ) )
take r = r; :: thesis: ex i0 being Element of Seg d st
( A = cell l,r & l . i0 = r . i0 & l . i0 in G . i0 & ( for i being Element of Seg d st i <> i0 holds
( l . i < r . i & [(l . i),(r . i)] is Gap of G . i ) ) )
consider X being Subset of (Seg d) such that
A4: ( 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 ) ) ) ) by A1, A3;
card ((Seg d) \ X) = (card (Seg d)) - (card X) by CARD_2:63
.= d - d' by A4, FINSEQ_1:78
.= 1 by A1 ;
then consider i0 being set such that
A5: (Seg d) \ X = {i0} by CARD_2:60;
i0 in (Seg d) \ X by A5, TARSKI:def 1;
then reconsider i0 = i0 as Element of Seg d by XBOOLE_0:def 5;
take i0 = i0; :: thesis: ( A = cell l,r & l . i0 = r . i0 & l . i0 in G . i0 & ( for i being Element of Seg d st i <> i0 holds
( l . i < r . i & [(l . i),(r . i)] is Gap of G . i ) ) )

A6: now

let i be Element of Seg d; :: thesis: ( i in X iff i <> i0 )
( i in (Seg d) \ X iff i = i0 ) by A5, TARSKI:def 1;
hence ( i in X iff i <> i0 ) by XBOOLE_0:def 5; :: thesis: verum

end;

thus A = cell l,r by A3; :: thesis: ( l . i0 = r . i0 & l . i0 in G . i0 & ( for i being Element of Seg d st i <> i0 holds
( l . i < r . i & [(l . i),(r . i)] is Gap of G . i ) ) )
not i0 in X by A6;
hence ( l . i0 = r . i0 & l . i0 in G . i0 ) by A4; :: thesis: for i being Element of Seg d st i <> i0 holds
( l . i < r . i & [(l . i),(r . i)] is Gap of G . i )
let i be Element of Seg d; :: thesis: ( i <> i0 implies ( l . i < r . i & [(l . i),(r . i)] is Gap of G . i ) )
assume i <> i0 ; :: thesis: ( l . i < r . i & [(l . i),(r . i)] is Gap of G . i )
then i in X by A6;
hence ( l . i < r . i & [(l . i),(r . i)] is Gap of G . i ) by A4; :: thesis: verum

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 & l . i0 in G . i0 & ( for i being Element of Seg d st i <> i0 holds
( l . i < r . i & [(l . i),(r . i)] is Gap of G . i ) ) ) ; :: thesis: A in cells d',G
reconsider X = (Seg d) \ {i0} as Subset of (Seg d) by XBOOLE_1:36;
( 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

thus card X = (card (Seg d)) - (card {i0}) by CARD_2:63
.= d - (card {i0}) by FINSEQ_1:78
.= d - 1 by CARD_1:50
.= d' by A1 ; :: 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 ) )
let i be Element of Seg d; :: thesis: ( ( 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 ) )
( i in {i0} iff i = i0 ) by TARSKI:def 1;
hence ( ( 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 A7, XBOOLE_0:def 5; :: thesis: verum

end;

hence A in cells d',G by A2, A7, Th33; :: thesis: verum