theorem Th71: :: RINFSUP1:71

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