for L being ExtREAL_sequence st L is () holds
( sup (rng L) <> +infty iff ex K being Real st
( 0 < K & ( for n being Nat holds L . n <= K ) ) )