theorem :: NAT_2:22

for n being Integer holds
( n is odd iff n mod 2 = 1 )