:: deftheorem defines ZERO IDEA_1:def 1 :
for n being Nat holds ZERO n = n |-> FALSE;