take 1 ; :: thesis: not 1 is even
assume 1 is even ; :: thesis: contradiction
then ex k being Integer st 1 = 2 * k by Def1;
hence contradiction by INT_1:22; :: thesis: verum