for A being Ordinal holds
( A is limit_ordinal iff for B being Ordinal
for n being Nat st B in A holds
B +^ n in A )