:: deftheorem Def12 defines natural ORDINAL1:def 12 :
for A being object holds
( A is natural iff A in omega );