let A be non empty closed_interval Subset of REAL; :: thesis:
let f be Function of A,REAL; :: thesis:
assume A1: f | A is bounded ; :: thesis:
(lower_bound (rng f)) * (vol A) is LowerBound of rng (upper_sum_set f)

let r be ExtReal; :: according to XXREAL_2:def 2 :: thesis:
assume r in rng (upper_sum_set f) ; :: thesis:
then consider D being Element of divs A such that
D in dom (upper_sum_set f) and
A2: (upper_sum_set f) . D = r by PARTFUN1:3;
reconsider D = D as Division of A by INTEGRA1:def 3;
r = upper_sum (f,D) by A2, INTEGRA1:def 10;
then A3: lower_sum (f,D) <= r by A1, INTEGRA1:28;
(lower_bound (rng f)) * (vol A) <= lower_sum (f,D) by A1, INTEGRA1:25;
hence (lower_bound (rng f)) * (vol A) <= r by A3, XXREAL_0:2; :: thesis:

end;

then rng (upper_sum_set f) is bounded_below ;
hence f is upper_integrable by INTEGRA1:def 12; :: thesis:
(upper_bound (rng f)) * (vol A) is UpperBound of rng (lower_sum_set f)

let r be ExtReal; :: according to XXREAL_2:def 1 :: thesis:
assume r in rng (lower_sum_set f) ; :: thesis:
then consider D being Element of divs A such that
D in dom (lower_sum_set f) and
A4: (lower_sum_set f) . D = r by PARTFUN1:3;
reconsider D = D as Division of A by INTEGRA1:def 3;
r = lower_sum (f,D) by A4, INTEGRA1:def 11;
then A5: upper_sum (f,D) >= r by A1, INTEGRA1:28;
(upper_bound (rng f)) * (vol A) >= upper_sum (f,D) by A1, INTEGRA1:27;
hence r <= (upper_bound (rng f)) * (vol A) by A5, XXREAL_0:2; :: thesis:

end;

then rng (lower_sum_set f) is bounded_above ;
hence f is lower_integrable by INTEGRA1:def 13; :: thesis: