theorem Th50: :: RINFSUP1:50

for seq being Real_Sequence st seq is bounded_below holds
inferior_realsequence seq is non-decreasing by Th48;