theorem Th22: :: BORSUK_4:25

for X being Subset of I[01]
for X9 being Subset of REAL st X9 = X holds
( X9 is bounded_above & X9 is bounded_below )