theorem Th59: :: NUMBER10:59
for i being Integer holds
( not i is even or (i ^2) mod 8 = 0 or (i ^2) mod 8 = 4 )