theorem Th9: :: NUMBER07:9

for n being Nat holds
( not n divides 2 or n = 1 or n = 2 ) by XPRIMES1:2;