assume a + b is integer ; :: thesis: contradiction
then (a + b) - b is integer ;
hence contradiction ; :: thesis: verum