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