theorem Th51: :: RINFSUP1:51

for seq being Real_Sequence st seq is bounded_above holds
superior_realsequence seq is non-increasing by Th49;