let seq be Real_Sequence; :: thesis: ( seq is bounded implies ex seq1 being Real_Sequence st
( seq1 is subsequence of seq & seq1 is convergent ) )
assume A1: seq is bounded ; :: thesis: ex seq1 being Real_Sequence st
( seq1 is subsequence of seq & seq1 is convergent )
consider Nseq being V45() sequence of NAT such that
A2: seq * Nseq is monotone by Th39;
take seq1 = seq * Nseq; :: thesis: ( seq1 is subsequence of seq & seq1 is convergent )
thus seq1 is subsequence of seq ; :: thesis: seq1 is convergent
thus seq1 is convergent by A1, A2, Th36, SEQM_3:29; :: thesis: verum