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