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 real-bounded & X is closed ) by A2, Th10;
hence ( upper_bound X in X & lower_bound X in X ) by A1, Th12, Th13; :: thesis: verum