take 0 ; :: thesis: ( 0 is even & 0 is natural )
0 = 2 * 0 ;
hence ( 0 is even & 0 is natural ) ; :: thesis: verum