theorem Th22: :: RFINSEQ2:24

for f being FinSequence of REAL st f is non-increasing holds
- f is non-decreasing