assume A1: (a ^2) -' 1 is square ; :: thesis: contradiction
a >= 2 by NAT_2:29;
then A2: a ^2 >= 2 * 2 by XREAL_1:66;
A3: (a ^2) -' 1 = (a ^2) - 1 by XREAL_1:233, NAT_1:14;
then not (a ^2) -' 1 is zero by A2;
then not ((a ^2) -' 1) + 1 is square by A1;
hence contradiction by A3; :: thesis: verum