theorem :: RINFSUP1:69

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