for n being Nat holds
( n in OddNAT iff n is odd )