theorem Th8: :: SEQM_3:8

for seq being Real_Sequence holds
( seq is non-increasing iff for n, m being Nat st n <= m holds
seq . m <= seq . n )