theorem Th19: :: RFINSEQ:19

for R being FinSequence of REAL holds
( R is non-increasing iff for n, m being Nat st n in dom R & m in dom R & n < m holds
R . n >= R . m )