let x be Real; :: thesis: (x ^2) + 1 > 0
x ^2 >= 0 by XREAL_1:63;
hence (x ^2) + 1 > 0 ; :: thesis: verum