set m1 = the Integer;
assume a + b is rational ; :: thesis: contradiction
then consider m, n being Integer such that
n <> 0 and
A1: a + b = m / n by RAT_1:2;
(a + b) - a = ((m * the Integer) - ( the Integer * n)) / ( the Integer * n) by A1;
hence contradiction ; :: thesis: verum