let A be non empty 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 A1: g | A is bounded ; :: thesis: upper_bound (rng g) >= lower_bound (rng g)
then A2: rng g is bounded_below by INTEGRA1:11;
rng g is bounded_above by A1, INTEGRA1:13;
hence upper_bound (rng g) >= lower_bound (rng g) by A2, SEQ_4:11; :: thesis: verum