let X be Subset of REAL ; :: thesis: ( X <> {} & X is compact implies ( upper_bound X in X & lower_bound X in X ) )
assume that
A1: X <> {} and
A2: X is compact ; :: thesis: ( upper_bound X in X & lower_bound X in X )
( X is bounded & X is closed ) by A2, Th28;
hence ( upper_bound X in X & lower_bound X in X ) by A1, Th30, Th31; :: thesis: verum