theorem :: NAT_D:12

for n being natural Number holds
( n mod 2 = 0 or n mod 2 = 1 )