theorem Th4: :: MESFUN10:4

for seq being ExtREAL_sequence
for a being R_eal st ( for n being Nat holds seq . n >= a ) holds
inf seq >= a