theorem :: XXREAL_2:73

for A being ext-real-membered set holds
( A is bounded_above iff sup A <> +infty )