theorem Th9: :: NUMBER08:9

for n being Nat holds
( not n divides 9 or n = 1 or n = 3 or n = 9 )