for L being ExtREAL_sequence st ( for n, m being Nat st n <= m holds
L . n <= L . m ) holds
( L is convergent & lim L = sup (rng L) )