theorem Th42: :: RINFSUP1:42

for n being Nat
for r being Real
for seq being Real_Sequence st seq is bounded_below holds
( ( for k being Nat holds r <= seq . (n + k) ) iff r <= (inferior_realsequence seq) . n )