theorem :: NAT_2:17

for n being Nat st n > 0 holds
(2 to_power n) mod 2 = 0