theorem Th11: :: INTEGRA1:13

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