for A being Ordinal ex B, C being Ordinal st
( B is limit_ordinal & C is natural & A = B +^ C )