let A be closed-interval Subset of REAL ; :: thesis: for g being Function of A,REAL st g | A is bounded holds
upper_bound (rng g) >= lower_bound (rng g)
let g be Function of A,REAL ; :: thesis: ( g | A is bounded implies upper_bound (rng g) >= lower_bound (rng g) )
assume g | A is bounded ; :: thesis: upper_bound (rng g) >= lower_bound (rng g)
then ( g | A is bounded_below & g | A is bounded_above ) ;
then ( rng g is bounded_above & rng g is bounded_below ) by INTEGRA1:13, INTEGRA1:15;
then rng g is bounded ;
hence upper_bound (rng g) >= lower_bound (rng g) by SEQ_4:24; :: thesis: verum