theorem Th52: :: FIB_NUM2:52
for k being Element of NAT holds
( (2 * k) + 1 in OddNAT & not 2 * k in OddNAT )