take 1 ; :: thesis: not 1 is even
let k be Element of NAT ; :: according to ABIAN:def 2 :: thesis: not 1 = 2 * k
thus not 1 = 2 * k by NAT_1:15; :: thesis: verum