theorem Th3: :: SEQM_3:3

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