consider b being Nat such that
A1: a = b ^2 by PYTHTRIP:def 3;
a = b * b by A1, SQUARE_1:def 1;
then b > 0 ;
then A2: ((b * b) + 1) + (2 * b) > ((b * b) + 1) + 0 by XREAL_1:6;
A3: ( b * b = b ^2 & (b + 1) * (b + 1) = (b + 1) ^2 ) by SQUARE_1:def 1;
(b * b) + 1 > (b * b) + 0 by XREAL_1:6;
then for k being Nat holds not (b ^2) + 1 = k ^2 by A2, A3, LmNAT;
hence not a + 1 is square by A1, PYTHTRIP:def 3; :: thesis: verum