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

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

end;

now

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

end;

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