:: deftheorem Def2 defines zero CHAIN_1:def 2 :
for d being Nat holds
( d is zero iff not d >= 1 );