take 1 ; :: thesis: 1 is odd
let k be Nat; :: according to ABIAN:def 2 :: thesis: not 1 = 2 * k
thus not 1 = 2 * k by NAT_1:15; :: thesis: verum