:: deftheorem Def9 defines is_limes_of ORDINAL2:def 9 :
for A being Ordinal
for fi being Ordinal-Sequence holds
( ( A = 0 implies ( A is_limes_of fi iff ex B being Ordinal st
( B in dom fi & ( for C being Ordinal st B c= C & C in dom fi holds
fi . C = 0 ) ) ) ) & ( not A = 0 implies ( A is_limes_of fi iff for B, C being Ordinal st B in A & A in C holds
ex D being Ordinal st
( D in dom fi & ( for E being Ordinal st D c= E & E in dom fi holds
( B in fi . E & fi . E in C ) ) ) ) ) );