for R being finite Subset of REAL st R <> {} holds
( R is bounded_above & upper_bound R in R & R is bounded_below & lower_bound R in R )