for L being ExtREAL_sequence
for K being R_eal st ( for n being Nat holds L . n <= K ) holds
sup (rng L) <= K