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