A1: omega is limit_ordinal by Def12;
a in omega by Def13;
hence succ a in omega by A1, Th41; :: according to ORDINAL1:def 13 :: thesis: verum