theorem :: RINFSUP1:23

for seq being Real_Sequence st seq is non-increasing & seq is bounded_below holds
seq is bounded ;