let A be closed-interval Subset of REAL; :: thesis: ( A is bounded_below & A is bounded_above )
A is bounded by RCOMP_1:28;
hence ( A is bounded_below & A is bounded_above ) ; :: thesis: verum