let X be Subset of I[01] ; :: 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 A1: X' = X ; :: thesis: ( X' is bounded_above & X' is bounded_below )
then for r being real number st r in X' holds
r <= 1 by BORSUK_1:86;
hence X' is bounded_above by SEQ_4:def 1; :: thesis: X' is bounded_below
for r being real number st r in X' holds
0 <= r by A1, BORSUK_1:86;
hence X' is bounded_below by SEQ_4:def 2; :: thesis: verum