let seq be Real_Sequence; :: thesis: ( seq is bounded implies ( superior_realsequence seq is convergent & lim (superior_realsequence seq) = lower_bound (superior_realsequence seq) ) )
assume seq is bounded ; :: thesis: ( superior_realsequence seq is convergent & lim (superior_realsequence seq) = lower_bound (superior_realsequence seq) )
then ( superior_realsequence seq is non-increasing & superior_realsequence seq is bounded ) by Th51, Th56;
hence ( superior_realsequence seq is convergent & lim (superior_realsequence seq) = lower_bound (superior_realsequence seq) ) by Th25; :: thesis: verum