let A be non empty closed_interval Subset of REAL; :: thesis: ( A is bounded_below & A is bounded_above )
A is real-bounded by RCOMP_1:10;
hence ( A is bounded_below & A is bounded_above ) ; :: thesis: verum