for n0 being non zero Nat st n0 is even holds
ex k, m being Nat st
( m is odd & k > 0 & n0 = (2 |^ k) * m )