theorem :: NAT_LAT:4

0_NN = 1 ;