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

end;

b = upper_sum f,D1 by A4, A5, Def11;
hence lower_integral f <= b by A1, A6, SEQ_4:62; :: thesis: verum

end;

not dom (upper_sum_set f) is empty by Def11;
then not rng (upper_sum_set f) is empty by RELAT_1:65;
hence upper_integral f >= lower_integral f by A3, SEQ_4:60; :: thesis: verum