let X be compact Subset of R^1; :: thesis: for X9 being Subset of REAL st X9 = X holds
( X9 is bounded_above & X9 is bounded_below )
let X9 be Subset of REAL; :: thesis: ( X9 = X implies ( X9 is bounded_above & X9 is bounded_below ) )
assume X9 = X ; :: thesis: ( X9 is bounded_above & X9 is bounded_below )
then X9 is compact by JORDAN5A:25;
then X9 is real-bounded by RCOMP_1:10;
hence ( X9 is bounded_above & X9 is bounded_below ) by XXREAL_2:def 11; :: thesis: verum