let R be finite Subset of REAL; :: thesis: ( R <> {} implies ( R is bounded_above & upper_bound R in R & R is bounded_below & lower_bound R in R ) )
assume A1: R <> {} ; :: thesis: ( R is bounded_above & upper_bound R in R & R is bounded_below & lower_bound R in R )
S₁[ card R] by Lm9;
hence ( R is bounded_above & upper_bound R in R & R is bounded_below & lower_bound R in R ) by A1; :: thesis: verum