take 0 ; :: thesis: 0 is even
take 0 ; :: according to ABIAN:def 2 :: thesis: 0 = 2 * 0
thus 0 = 2 * 0 ; :: thesis: verum