theorem :: ORDINAL1:29

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