theorem Th9: :: NUMPOLY1:9

for n being Nat holds
not not n, 0 are_congruent_mod 10 & ... & not n,9 are_congruent_mod 10