let A be closed-interval Subset of REAL ; :: thesis: for f being Function of A,REAL st f | A is bounded holds
rng (upper_sum_set f) is bounded_below
let f be Function of A,REAL ; :: thesis: ( f | A is bounded implies rng (upper_sum_set f) is bounded_below )
assume A1: f | A is bounded ; :: thesis: rng (upper_sum_set f) is bounded_below
set D1 = the Division of A;
for a being real number st a in rng (upper_sum_set f) holds
a >= lower_sum f,the Division of A

proof

let a be real number ; :: thesis: ( a in rng (upper_sum_set f) implies a >= lower_sum f,the Division of A )
assume a in rng (upper_sum_set f) ; :: thesis: a >= lower_sum f,the Division of A
then consider D being Element of divs A such that
A2: ( D in dom (upper_sum_set f) & a = (upper_sum_set f) . D ) by PARTFUN1:26;
reconsider D = D as Division of A by INTEGRA1:def 3;
a = upper_sum f,D by A2, INTEGRA1:def 11;
hence a >= lower_sum f,the Division of A by A1, INTEGRA1:50; :: thesis: verum

end;

hence rng (upper_sum_set f) is bounded_below by SEQ_4:def 2; :: thesis: verum