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