for seq, seq1 being Real_Sequence st seq is increasing & seq1 is subsequence of seq holds
seq1 is increasing