let X be Subset of I[01]; :: 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 A1: X9 = X ; :: thesis: ( X9 is bounded_above & X9 is bounded_below )
then for r being ExtReal st r in X9 holds
r <= 1 by BORSUK_1:43;
then 1 is UpperBound of X9 by XXREAL_2:def 1;
hence X9 is bounded_above by XXREAL_2:def 10; :: thesis: X9 is bounded_below
for r being ExtReal st r in X9 holds
0 <= r by A1, BORSUK_1:43;
then 0 is LowerBound of X9 by XXREAL_2:def 2;
hence X9 is bounded_below by XXREAL_2:def 9; :: thesis: verum