let A be closed-interval Subset of REAL; :: thesis: for f being Function of A,REAL st f | A is bounded holds
( f is upper_integrable & f is lower_integrable )
let f be Function of A,REAL; :: thesis: ( f | A is bounded implies ( f is upper_integrable & f is lower_integrable ) )
assume A1: f | A is bounded ; :: thesis: ( f is upper_integrable & f is lower_integrable )
(lower_bound (rng f)) * (vol A) is LowerBound of rng (upper_sum_set f)

proof

let r be ext-real number ; :: according to XXREAL_2:def 2 :: thesis: ( not r in rng (upper_sum_set f) or (lower_bound (rng f)) * (vol A) <= r )
assume r in rng (upper_sum_set f) ; :: thesis: (lower_bound (rng f)) * (vol A) <= r
then consider D being Element of divs A such that
A2: D in dom (upper_sum_set f) and
A3: (upper_sum_set f) . D = r by PARTFUN1:26;
reconsider D = D as Division of A by INTEGRA1:def 3;
r = upper_sum (f,D) by A2, A3, INTEGRA1:def 11;
then A4: lower_sum (f,D) <= r by A1, INTEGRA1:30;
(lower_bound (rng f)) * (vol A) <= lower_sum (f,D) by A1, INTEGRA1:27;
hence (lower_bound (rng f)) * (vol A) <= r by A4, XXREAL_0:2; :: thesis: verum

end;

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

proof

let r be ext-real number ; :: according to XXREAL_2:def 1 :: thesis: ( not r in rng (lower_sum_set f) or r <= (upper_bound (rng f)) * (vol A) )
assume r in rng (lower_sum_set f) ; :: thesis: r <= (upper_bound (rng f)) * (vol A)
then consider D being Element of divs A such that
A5: D in dom (lower_sum_set f) and
A6: (lower_sum_set f) . D = r by PARTFUN1:26;
reconsider D = D as Division of A by INTEGRA1:def 3;
r = lower_sum (f,D) by A5, A6, INTEGRA1:def 12;
then A7: upper_sum (f,D) >= r by A1, INTEGRA1:30;
(upper_bound (rng f)) * (vol A) >= upper_sum (f,D) by A1, INTEGRA1:29;
hence r <= (upper_bound (rng f)) * (vol A) by A7, XXREAL_0:2; :: thesis: verum

end;

then rng (lower_sum_set f) is bounded_above by XXREAL_2:def 10;
hence f is lower_integrable by INTEGRA1:def 14; :: thesis: verum