theorem Th65: :: RINFSUP1:65

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