:: deftheorem Def14 defines zero ORDINAL1:def 14 :
for x being Number holds
( x is zero iff x = 0 );