theorem :: RINFSUP1:70

for seq being Real_Sequence st seq is non-increasing holds
superior_realsequence seq = seq