take succ {} ; :: thesis: ( not succ {} is empty & succ {} is natural )
thus not succ {} is empty ; :: thesis: succ {} is natural
( omega is limit_ordinal & {} in omega ) by Def11;
hence succ {} in omega by Th24; :: according to ORDINAL1:def 12 :: thesis: verum