theorem :: NUMBER14:17

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