let a, b be Real; :: thesis: for f being real-valued Function st rng f c= [.a,b.] holds
f is bounded
let f be real-valued Function; :: thesis: ( rng f c= [.a,b.] implies f is bounded )
assume A1: rng f c= [.a,b.] ; :: thesis: f is bounded
( [.a,b.] c= [.a,+infty.[ & [.a,b.] c= ].-infty,b.] ) by XXREAL_1:251, XXREAL_1:265;
then ( rng f c= [.a,+infty.[ & rng f c= ].-infty,b.] ) by A1;
then ( rng f is bounded_below & rng f is bounded_above ) by XXREAL_2:43, XXREAL_2:44;
then ( f is bounded_below & f is bounded_above ) by INTEGRA1:12, INTEGRA1:14;
hence f is bounded ; :: thesis: verum