for A being Ordinal holds
( not A is limit_ordinal iff ex B being Ordinal st A = succ B )