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