theorem Th51: :: FIB_NUM2:51

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