theorem Th5: :: SEQM_3:5

for seq being Real_Sequence holds
( seq is non-decreasing iff for n, k being Nat holds seq . n <= seq . (n + k) ) by Lm4;