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 real number st r in X9 holds
r <= 1 by BORSUK_1:86;
hence X9 is bounded_above by SEQ_4:def 1; :: thesis: X9 is bounded_below
for r being real number st r in X9 holds
0 <= r by A1, BORSUK_1:86;
hence X9 is bounded_below by SEQ_4:def 2; :: thesis: verum