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 ex p being Element of NAT st 2 * k = (2 * p) + 1 ;
hence contradiction ; :: thesis: verum