theorem :: RINFSUP1:69

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