theorem Th8: :: NUMERAL2:8

EvenNAT \/ OddNAT = NAT