theorem Th14: :: INTEGR20:14

for n being Nat ex k being Nat st
( n = 2 * k or n = (2 * k) + 1 )