take succ {} ; :: thesis: ( not succ {} is empty & succ {} is natural )
thus not succ {} is empty ; :: thesis: succ {} is natural
A1: omega is limit_ordinal by Def12;
{} in omega by Def13;
hence succ {} in omega by A1, Th41; :: according to ORDINAL1:def 13 :: thesis: verum