theorem Th24: :: RINFSUP1:24

for seq being Real_Sequence st seq is non-decreasing & seq is bounded_above holds
lim seq = upper_bound seq