for X being compact Subset of R^1
for X9 being Subset of REAL st X9 = X holds
( X9 is bounded_above & X9 is bounded_below )