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