let seq be Real_Sequence; :: thesis: ( seq is bounded implies ( inferior_realsequence seq is convergent & lim (inferior_realsequence seq) = upper_bound (inferior_realsequence seq) ) )
assume seq is bounded ; :: thesis: ( inferior_realsequence seq is convergent & lim (inferior_realsequence seq) = upper_bound (inferior_realsequence seq) )
then ( inferior_realsequence seq is non-decreasing & inferior_realsequence seq is bounded ) by Th50, Th56;
hence ( inferior_realsequence seq is convergent & lim (inferior_realsequence seq) = upper_bound (inferior_realsequence seq) ) by Th24; :: thesis: verum