let p be Nat; :: thesis: ( p > 2 & p is prime implies not p is even )
assume A1: ( p > 2 & p is prime ) ; :: thesis: not p is even
assume p is even ; :: thesis: contradiction
then p mod 2 = 0 by NAT_2:23;
then consider k being Nat such that
A2: ( p = (2 * k) + 0 & 0 < 2 ) by NAT_D:def 2;
2 divides p by A2, NAT_D:def 3;
hence contradiction by A1, INT_2:def 5; :: thesis: verum