take 1 ; :: thesis: not 1 is even
assume 1 is even ; :: thesis: contradiction
then consider k being Integer such that
A1: 1 = 2 * k by Def1;
thus contradiction by A1, INT_1:22; :: thesis: verum