theorem Th78: :: NUMBER15:78

for n being Nat holds
( not n is even or n mod 4 = 0 or n mod 4 = 2 )