for A being Ordinal holds
( A is limit_ordinal iff for C being Ordinal st C in A holds
succ C in A )