theorem :: SEQM_3:2

for seq being Real_Sequence holds
( seq is increasing iff for n, k being Nat holds seq . n < seq . ((n + 1) + k) ) by Lm2;