for seq, seq1 being Real_Sequence st seq is monotone & seq1 is subsequence of seq holds
seq1 is monotone by Th25, Th24;