theorem Th56: :: MESFUNC5:56

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