theorem Th48: :: RINFSUP1:48

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