:: deftheorem defines 0_NN NAT_LAT:def 4 :
0_NN = 1;