theorem :: NUMBER14:18

for i, j being Integer st i,j are_congruent_mod 2 holds
( i is even iff j is even ) ;