let X be compact Subset of R^1 ; :: thesis: for X' being Subset of REAL st X' = X holds
( X' is bounded_above & X' is bounded_below )
let X' be Subset of REAL ; :: thesis: ( X' = X implies ( X' is bounded_above & X' is bounded_below ) )
assume X' = X ; :: thesis: ( X' is bounded_above & X' is bounded_below )
then X' is compact by TOPREAL6:81;
then X' is bounded by RCOMP_1:28;
hence ( X' is bounded_above & X' is bounded_below ) by XXREAL_2:def 11; :: thesis: verum