let k be Element of NAT ; :: thesis: ( (2 * k) + 1 in OddNAT & not 2 * k in OddNAT )
thus (2 * k) + 1 in OddNAT ; :: thesis: not 2 * k in OddNAT
assume 2 * k in OddNAT ; :: thesis: contradiction
then consider p being Element of NAT such that
A1: 2 * k = (2 * p) + 1 ;
thus contradiction by A1; :: thesis: verum