theorem Th60: :: MESFUNC5:60

for L being ExtREAL_sequence
for c being ExtReal st ( for n being Nat holds L . n = c ) holds
( L is convergent & lim L = c & lim L = sup (rng L) )