theorem Th21: :: NAT_2:21

for n being Integer holds
( n is even iff n mod 2 = 0 )