theorem :: INTEGRA1:14

for f being real-valued Function st rng f is bounded_above holds
f is bounded_above