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