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