:: deftheorem defines zero CHAIN_1:def 1 :
for d being real Element of NAT holds
( d is zero iff not d > 0 );