defpred S₁[ Element of Seg d, Element of REAL ] means ( $2 in G . $1 & ( for xi being Real st xi in G . $1 holds
xi <= $2 ) );
A1: for i being Element of Seg d ex li being Element of REAL st S₁[i,li] by Th9;
consider l being Function of (Seg d),REAL such that
A2: for i being Element of Seg d holds S₁[i,l . i] from FUNCT_2:sch 3(A1);
reconsider l = l as Element of REAL d by Def3;
defpred S₂[ Element of Seg d, Element of REAL ] means ( $2 in G . $1 & ( for xi being Real st xi in G . $1 holds
xi >= $2 ) );
A3: for i being Element of Seg d ex ri being Element of REAL st S₂[i,ri] by Th10;
consider r being Function of (Seg d),REAL such that
A4: for i being Element of Seg d holds S₂[i,r . i] from FUNCT_2:sch 3(A3);
reconsider r = r as Element of REAL d by Def3;

A5: now :: thesis: for i being Element of Seg d holds r . i < l . i

let i be Element of Seg d; :: thesis: r . i < l . i
r . i in G . i by A4;
then A6: r . i <= l . i by A2;

now :: thesis: not l . i = r . i

assume A7: l . i = r . i ; :: thesis: contradiction
consider x1, x2 being object such that
A8: x1 in G . i and
A9: x2 in G . i and
A10: x1 <> x2 by ZFMISC_1:def 10;
reconsider x1 = x1, x2 = x2 as Element of REAL by A8, A9;
A11: r . i <= x1 by A4, A8;
A12: x1 <= l . i by A2, A8;
A13: r . i <= x2 by A4, A9;
A14: x2 <= l . i by A2, A9;
x1 = l . i by A7, A11, A12, XXREAL_0:1;
hence contradiction by A7, A10, A13, A14, XXREAL_0:1; :: thesis: verum

end;

hence r . i < l . i by A6, XXREAL_0:1; :: thesis: verum

end;

A15: 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 )
A16: l . i in G . i by A2;
A17: r . i in G . i by A4;
A18: r . i < l . i by A5;
for xi being Real st xi in G . i holds
( not l . i < xi & not xi < r . i ) by A2, A4;
hence ( r . i < l . i & [(l . i),(r . i)] is Gap of G . i ) by A16, A17, A18, Th13; :: thesis: verum

end;

then reconsider A = cell (l,r) as Cell of d,G by Th30;
take A ; :: thesis: ex l, r being Element of REAL d st
( A = cell (l,r) & ( for i being Element of Seg d holds
( r . i < l . i & [(l . i),(r . i)] is Gap of G . i ) ) )
take l ; :: thesis: ex r being Element of REAL d st
( A = cell (l,r) & ( for i being Element of Seg d holds
( r . i < l . i & [(l . i),(r . i)] is Gap of G . i ) ) )
take r ; :: thesis: ( A = cell (l,r) & ( for i being Element of Seg d holds
( r . i < l . i & [(l . i),(r . i)] is Gap of G . i ) ) )
thus ( A = cell (l,r) & ( for i being Element of Seg d holds
( r . i < l . i & [(l . i),(r . i)] is Gap of G . i ) ) ) by A15; :: thesis: verum