theorem :: INTEGRA1:15

for f being real-valued Function st f is bounded holds
rng f is real-bounded by Th11, Th9;