for k being Element of NAT holds
( (2 * k) + 1 in OddNAT & not 2 * k in OddNAT )