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