for F being sequence of ExtREAL
for n being Nat st F is nonnegative holds
( (Ser F) . n <= (Ser F) . (n + 1) & 0. <= (Ser F) . n )