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