for k being Nat holds
( 2 * k in EvenNAT & not (2 * k) + 1 in EvenNAT )