let A be Subset of REAL; :: thesis: ( not A is empty & A is closed_interval implies A is bounded )
assume ( not A is empty & A is closed_interval ) ; :: thesis: A is bounded
hence ( A is bounded_below & A is bounded_above ) by Th3; :: according to XXREAL_2:def 11 :: thesis: verum