:: deftheorem defines lim_inf ORDINAL2:def 8 :
for L being Sequence
for b₂ being Ordinal holds
( b₂ = lim_inf L iff ex fi being Ordinal-Sequence st
( b₂ = sup fi & dom fi = dom L & ( for A being Ordinal st A in dom L holds
fi . A = inf (rng (L | ((dom L) \ A))) ) ) );