let A be non empty closed_interval Subset of REAL; :: thesis: for f being Function of A,REAL st f | A is bounded holds
upper_integral f >= lower_integral f
let f be Function of A,REAL; :: thesis: ( f | A is bounded implies upper_integral f >= lower_integral f )
assume A1: f | A is bounded ; :: thesis: upper_integral f >= lower_integral f
A2: for b being Real st b in rng (upper_sum_set f) holds
lower_integral f <= b
proof
let b be Real; :: thesis: ( b in rng (upper_sum_set f) implies lower_integral f <= b )
assume b in rng (upper_sum_set f) ; :: thesis: lower_integral f <= b
then consider D1 being Element of divs A such that
D1 in dom (upper_sum_set f) and
A3: b = (upper_sum_set f) . D1 by PARTFUN1:3;
reconsider D1 = D1 as Division of A by Def2;
A4: for a being Real st a in rng (lower_sum_set f) holds
a <= upper_sum (f,D1)
proof
let a be Real; :: thesis: ( a in rng (lower_sum_set f) implies a <= upper_sum (f,D1) )
assume a in rng (lower_sum_set f) ; :: thesis: a <= upper_sum (f,D1)
then consider D2 being Element of divs A such that
D2 in dom (lower_sum_set f) and
A5: a = (lower_sum_set f) . D2 by PARTFUN1:3;
reconsider D2 = D2 as Division of A by Def2;
a = lower_sum (f,D2) by A5, Def10;
hence a <= upper_sum (f,D1) by A1, Th46; :: thesis: verum
end;
b = upper_sum (f,D1) by A3, Def9;
hence lower_integral f <= b by A4, SEQ_4:45; :: thesis: verum
end;
thus upper_integral f >= lower_integral f by A2, SEQ_4:43; :: thesis: verum