let I be non empty closed_interval Subset of REAL; :: thesis:
let f be bounded integrable Function of I,REAL; :: thesis:
let epsilon be Real; :: thesis:
assume that
A1: not I is trivial and
A4: 0 < epsilon ; :: thesis:
set J = integral f;
A6: rng (lower_sum_set f) is bounded_above by INTEGRA1:def 13, INTEGRA1:def 16;
A7: lower_integral f = upper_integral f by INTEGRA1:def 16;
A8: lower_integral f = upper_bound (rng (lower_sum_set f)) by INTEGRA1:def 15;
set X = rng (lower_sum_set f);
set e = epsilon / 2;
consider ru being Real such that
A10: ru in rng (lower_sum_set f) and
A11: (upper_bound (rng (lower_sum_set f))) - (epsilon / 2) < ru by A4, A6, SEQ_4:def 1;
consider x1 being object such that
A13: x1 in dom (lower_sum_set f) and
A14: ru = (lower_sum_set f) . x1 by A10, FUNCT_1:def 3;
reconsider x1 = x1 as Division of I by A13, INTEGRA1:def 3;
ru = lower_sum (f,x1) by A14, INTEGRA1:def 11;
then A15: (integral f) - (epsilon / 2) < lower_sum (f,x1) by A8, A7, INTEGRA1:def 17, A11;
A16: rng (upper_sum_set f) is bounded_below by INTEGRA1:def 12, INTEGRA1:def 16;
A17: upper_integral f = lower_bound (rng (upper_sum_set f)) by INTEGRA1:def 14;
set X2 = rng (upper_sum_set f);
consider rl being Real such that
A18: rl in rng (upper_sum_set f) and
A19: rl < (lower_bound (rng (upper_sum_set f))) + (epsilon / 2) by A4, A16, SEQ_4:def 2;
consider x2 being object such that
A20: x2 in dom (upper_sum_set f) and
A21: rl = (upper_sum_set f) . x2 by A18, FUNCT_1:def 3;
reconsider x2 = x2 as Division of I by A20, INTEGRA1:def 3;
rl = upper_sum (f,x2) by A21, INTEGRA1:def 10;
then A22: upper_sum (f,x2) < (integral f) + (epsilon / 2) by A17, INTEGRA1:def 17, A19;
consider x3 being Division of I such that
A23: x1 <= x3 and
A24: x2 <= x3 by INTEGRA1:47;

per cases ;

suppose A25: x3 . 1 = lower_bound I ; :: thesis:

A26: 2 <= len x3

proof

assume A27: len x3 < 2 ; :: thesis:
A28: upper_bound I = x3 . (len x3) by INTEGRA1:def 2
.= x3 . 1 by A27, NAT_1:23 ;
I = [.(x3 . 1),(x3 . 1).] by A25, A28, INTEGRA1:4;
then I = {(x3 . 1)} by XXREAL_1:17;
hence contradiction by A1; :: thesis:

end;

then reconsider x4 = x3 /^ 1 as Division of I by COUSIN:65;
take x4 ; :: thesis:

now :: thesis:

thus A29: x4 . 1 <> lower_bound I :: thesis:

proof

assume A30: x4 . 1 = lower_bound I ; :: thesis:
A31: 1 <= len x3 by A26, XXREAL_0:2;
then len (x3 /^ 1) = (len x3) - 1 by RFINSEQ:def 1;
then 2 - 1 <= ((len (x3 /^ 1)) + 1) - 1 by A26, XREAL_1:9;
then 1 in dom (x3 /^ 1) by FINSEQ_3:25;
then A32: x4 . 1 = x3 . (1 + 1) by A31, RFINSEQ:def 1;
( 1 <= len x3 & 2 <= len x3 ) by A26, XXREAL_0:2;
then ( 1 in dom x3 & 2 in dom x3 ) by FINSEQ_3:25;
hence contradiction by A32, A25, A30, VALUED_0:def 13; :: thesis:

end;

A33: ( upper_sum (f,x4) = upper_sum (f,x3) & lower_sum (f,x4) = lower_sum (f,x3) ) by A25, Th38;
( f | I is bounded_above & f | I is bounded_below ) ;
then A34: ( upper_sum (f,x4) <= upper_sum (f,x2) & lower_sum (f,x1) <= lower_sum (f,x4) ) by A33, A23, A24, INTEGRA1:45, INTEGRA1:46;
then ( upper_sum (f,x4) < (integral f) + (epsilon / 2) & (integral f) - (epsilon / 2) < lower_sum (f,x4) ) by A15, A22, XXREAL_0:2;
then (upper_sum (f,x4)) - (lower_sum (f,x4)) < 2 * (epsilon / 2) by Lm02;
hence ( x4 . 1 <> lower_bound I & upper_sum (f,x4) < (integral f) + (epsilon / 2) & (integral f) - (epsilon / 2) < lower_sum (f,x4) & (upper_sum (f,x4)) - (lower_sum (f,x4)) < epsilon ) by A34, A15, A22, XXREAL_0:2, A29; :: thesis:

end;

hence ( x4 . 1 <> lower_bound I & upper_sum (f,x4) < (integral f) + (epsilon / 2) & (integral f) - (epsilon / 2) < lower_sum (f,x4) & (upper_sum (f,x4)) - (lower_sum (f,x4)) < epsilon ) ; :: thesis:

end;

suppose A35: x3 . 1 <> lower_bound I ; :: thesis:

( f | I is bounded_above & f | I is bounded_below ) ;
then ( upper_sum (f,x3) <= upper_sum (f,x2) & lower_sum (f,x1) <= lower_sum (f,x3) ) by A23, A24, INTEGRA1:45, INTEGRA1:46;
then A36: ( upper_sum (f,x3) < (integral f) + (epsilon / 2) & (integral f) - (epsilon / 2) < lower_sum (f,x3) ) by A15, A22, XXREAL_0:2;
then (upper_sum (f,x3)) - (lower_sum (f,x3)) < 2 * (epsilon / 2) by Lm02;
hence ex D being Division of I st
( D . 1 <> lower_bound I & upper_sum (f,D) < (integral f) + (epsilon / 2) & (integral f) - (epsilon / 2) < lower_sum (f,D) & (upper_sum (f,D)) - (lower_sum (f,D)) < epsilon ) by A36, A35; :: thesis:

end;