( omega is limit_ordinal & a in omega ) by Def12, Def13;
hence succ a in omega by Th41; :: according to ORDINAL1:def 12 :: thesis: verum