theorem :: RINFSUP1:22

for seq being Real_Sequence st seq is non-decreasing & seq is bounded_above holds
seq is bounded ;