theorem Th24: :: SEQM_3:24

for seq, seq1 being Real_Sequence st seq is non-decreasing & seq1 is subsequence of seq holds
seq1 is non-decreasing