theorem :: RINFSUP1:63

for n being Nat
for seq being Real_Sequence st seq is non-decreasing holds
seq . n <= (inferior_realsequence seq) . (n + 1)