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 ex k being Nat st
( p = (2 * k) + 0 & 0 < 2 ) by NAT_D:def 2;
then 2 divides p by NAT_D:def 3;
hence contradiction by A1, INT_2:def 5; :: thesis: verum