theorem Th6: :: SEQM_3:6

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