let k be Nat; :: thesis: ( 2 * k in EvenNAT & not (2 * k) + 1 in EvenNAT )
thus 2 * k in EvenNAT ; :: thesis: not (2 * k) + 1 in EvenNAT
assume (2 * k) + 1 in EvenNAT ; :: thesis: contradiction
then ex p being Nat st (2 * k) + 1 = 2 * p ;
hence contradiction ; :: thesis: verum