theorem Th37: :: RINFSUP2:37

for seq being ExtREAL_sequence st seq is non-decreasing holds
( seq is convergent & lim seq = sup seq )