theorem Th81: :: NUMBER15:81

for n being Nat holds
( not n is odd or n,1 are_congruent_mod 4 or n,3 are_congruent_mod 4 )