theorem Th80: :: NUMBER15:80

for n being Nat holds
( not n is odd or n mod 4 = 1 or n mod 4 = 3 )