let k be Element of 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 consider p being Element of NAT such that
A1: (2 * k) + 1 = 2 * p ;
thus contradiction by A1; :: thesis: verum