let seq, seq1 be Real_Sequence; :: thesis: ( seq is monotone & seq1 is subsequence of seq implies seq1 is monotone )
assume that
A1: seq is monotone and
A2: seq1 is subsequence of seq ; :: thesis: seq1 is monotone

A3: now :: thesis: ( seq is non-increasing implies seq1 is monotone )

assume seq is non-increasing ; :: thesis: seq1 is monotone
then seq1 is non-increasing by A2, Th25;
hence seq1 is monotone by Def5; :: thesis: verum

end;

now :: thesis: ( seq is non-decreasing implies seq1 is monotone )

assume seq is non-decreasing ; :: thesis: seq1 is monotone
then seq1 is non-decreasing by A2, Th24;
hence seq1 is monotone by Def5; :: thesis: verum

end;

hence seq1 is monotone by A1, A3, Def5; :: thesis: verum