theorem Th42: :: RINFSUP1:42

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