let A be non empty 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 ExtReal; :: 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
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: verum

end;

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

proof

let r be ExtReal; :: 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
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: verum

end;

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