a > 1 by NEWTON03:def 1;
then a >= 1 + 1 by INT_1:7;
hence max (a,2) = a by XXREAL_0:def 10; :: thesis: verum