2 = 2 * 1 ;
then reconsider t = 2 as even Integer ;
m + t is odd ;
hence not m + 2 is even ; :: thesis: verum