theorem :: RINFSUP1:64

for seq being Real_Sequence st seq is non-decreasing holds
inferior_realsequence seq = seq