let a, b be Real; for f being real-valued Function st rng f c= [.a,b.] holds
f is bounded
let f be real-valued Function; ( rng f c= [.a,b.] implies f is bounded )
assume A1:
rng f c= [.a,b.]
; 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
; verum