let seq, seq1 be Real_Sequence; :: thesis: ( seq is bounded & seq1 is subsequence of seq implies seq1 is bounded )
assume A1: ( seq is bounded & seq1 is subsequence of seq ) ; :: thesis: seq1 is bounded
hence seq1 is bounded_above by Th56; :: according to SEQ_2:def 8 :: thesis: seq1 is bounded_below
thus seq1 is bounded_below by A1, Th57; :: thesis: verum