theorem :: INTEGRA1:12

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