theorem :: COMSEQ_3:50

for seq being Complex_Sequence st seq is bounded holds
ex seq1 being Complex_Sequence st
( seq1 is subsequence of seq & seq1 is convergent )