2 = 2 * 1 ;
hence 2 is even ; :: thesis: verum