theorem :: PEPIN:17

for p being Nat st p > 2 & p is prime holds
p is odd