let p be Nat; :: thesis: ( p > 2 & p is prime implies p is odd )
assume A1: ( p > 2 & p is prime ) ; :: thesis: p is odd
assume p is even ; :: thesis: contradiction
then p mod 2 = 0 by NAT_2:21;
then ex k being Nat st
( p = (2 * k) + 0 & 0 < 2 ) by NAT_D:def 2;
then 2 divides p ;
hence contradiction by A1, INT_2:def 4; :: thesis: verum