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 A2: f | A is bounded ; :: thesis: upper_integral f >= lower_integral f
A3: for b being real number st b in rng (upper_sum_set f) holds
lower_integral f <= b

proof

let b be real number ; :: 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
A5: b = (upper_sum_set f) . D1 by PARTFUN1:3;
reconsider D1 = D1 as Division of A by Def3;
A6: for a being real number st a in rng (lower_sum_set f) holds
a <= upper_sum (f,D1)

proof

let a be real number ; :: 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
A8: a = (lower_sum_set f) . D2 by PARTFUN1:3;
reconsider D2 = D2 as Division of A by Def3;
a = lower_sum (f,D2) by A8, Def12;
hence a <= upper_sum (f,D1) by A2, Th50; :: thesis: verum

end;

b = upper_sum (f,D1) by A5, Def11;
hence lower_integral f <= b by A6, SEQ_4:45; :: thesis: verum

end;

thus upper_integral f >= lower_integral f by A3, SEQ_4:43; :: thesis: verum