theorem Th86: :: DBLSEQ_3:86

for seq being ExtREAL_sequence
for r being R_eal st ( for n being Nat holds seq . n <= r ) holds
lim_sup seq <= r