defpred S_{1}[ 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_{1}[i,li]
by Th9;

consider l being Function of (Seg d),REAL such that

A2: for i being Element of Seg d holds S_{1}[i,l . i]
from FUNCT_2:sch 3(A1);

reconsider l = l as Element of REAL d by Def3;

defpred S_{2}[ 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_{2}[i,ri]
by Th10;

consider r being Function of (Seg d),REAL such that

A4: for i being Element of Seg d holds S_{2}[i,r . i]
from FUNCT_2:sch 3(A3);

reconsider r = r as Element of REAL d by Def3;

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

xi <= $2 ) );

A1: for i being Element of Seg d ex li being Element of REAL st S

consider l being Function of (Seg d),REAL such that

A2: for i being Element of Seg d holds S

reconsider l = l as Element of REAL d by Def3;

defpred S

xi >= $2 ) );

A3: for i being Element of Seg d ex ri being Element of REAL st S

consider r being Function of (Seg d),REAL such that

A4: for i being Element of Seg d holds S

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;

end;r . i in G . i by A4;

then A6: r . i <= l . i by A2;

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

hence
r . i < l . i
by A6, XXREAL_0:1; :: thesis: verumassume 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;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

A15: now :: thesis: for i being Element of Seg d holds

( r . i < l . i & [(l . i),(r . i)] is Gap of G . i )

then reconsider A = cell (l,r) as Cell of d,G by Th30;( 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;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

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