theorem Th3: :: NUMPOLY1:3

for n being Nat holds
not not n mod 5 = 0 & ... & not n mod 5 = 4