let A be 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
not dom (upper_sum_set f) is empty by Def11;
then A2: not rng (upper_sum_set f) is empty by RELAT_1:65;
not dom (lower_sum_set f) is empty by Def12;
then A3: not rng (lower_sum_set f) is empty by RELAT_1:65;
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
A4: ( D1 in dom (upper_sum_set f) & b = (upper_sum_set f) . D1 ) by PARTFUN1:26;
reconsider D1 = D1 as Division of A by Def3;
A5: b = upper_sum f,D1 by A4, Def11;
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
A6: ( D2 in dom (lower_sum_set f) & a = (lower_sum_set f) . D2 ) by PARTFUN1:26;
reconsider D2 = D2 as Division of A by Def3;
a = lower_sum f,D2 by A6, Def12;
hence a <= upper_sum f,D1 by A1, Th50; :: thesis: verum

end;

hence lower_integral f <= b by A3, A5, SEQ_4:62; :: thesis: verum

end;

hence upper_integral f >= lower_integral f by A2, SEQ_4:60; :: thesis: verum