:: deftheorem Def10 defines lim ORDINAL2:def 10 :
for fi being Ordinal-Sequence st ex A being Ordinal st A is_limes_of fi holds
for b₂ being Ordinal holds
( b₂ = lim fi iff b₂ is_limes_of fi );