theorem Th5: :: MESFUN10:5

for seq being ExtREAL_sequence
for a being R_eal st ( for n being Nat holds seq . n <= a ) holds
sup seq <= a