let d' be Element of NAT ; :: thesis: for d being non zero Element of NAT
for l, r being Element of REAL d
for G being Grating of d st d = d' + 1 holds
( cell l,r in cells d',G iff ex i0 being Element of Seg d st
( 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 l, r being Element of REAL d
for G being Grating of d st d = d' + 1 holds
( cell l,r in cells d',G iff ex i0 being Element of Seg d st
( 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 l, r be Element of REAL d; :: thesis: for G being Grating of d st d = d' + 1 holds
( cell l,r in cells d',G iff ex i0 being Element of Seg d st
( 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 ( cell l,r in cells d',G iff ex i0 being Element of Seg d st
( 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: ( cell l,r in cells d',G iff ex i0 being Element of Seg d st
( 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 i0 being Element of Seg d st
( 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 cell l,r in cells d',G )

assume cell l,r in cells d',G ; :: thesis: ex i0 being Element of Seg d st
( 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, i0 being Element of Seg d such that
A2: cell l,r = cell l',r' and
A3: l' . i0 = r' . i0 and
A4: l' . i0 in G . i0 and
A5: for i being Element of Seg d st i <> i0 holds
( l' . i < r' . i & [(l' . i),(r' . i)] is Gap of G . i ) by A1, Th42;
take i0 = i0; :: 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 ) ) )

A6: now

let i be Element of Seg d; :: thesis: l' . i <= r' . i
( i = i0 or i <> i0 ) ;
hence l' . i <= r' . i by A3, A5; :: thesis: verum

end;

then A7: l = l' by A2, Th32;
r = r' by A2, A6, Th32;
hence ( 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 ) ) ) by A3, A4, A5, A7; :: thesis: verum

end;

thus ( ex i0 being Element of Seg d st
( 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 cell l,r in cells d',G ) by A1, Th42; :: thesis: verum