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