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

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