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