theorem :: XXREAL_2:74

for A being ext-real-membered set holds
( A is bounded_below iff inf A <> -infty )