theorem Th5: :: NUMPOLY1:5

for n being Nat holds
not not n, 0 are_congruent_mod 5 & ... & not n,4 are_congruent_mod 5