let a be Real; :: thesis: 1 + (a ^2) <> 0
assume A1: 1 + (a ^2) = 0 ; :: thesis: contradiction
then a ^2 = - 1 ;
then a = 0 by SQUARE_1:12;
hence contradiction by A1; :: thesis: verum