let x be real number ; :: thesis: (x ^2 ) + 1 > 0
x ^2 >= 0 by XREAL_1:65;
hence (x ^2 ) + 1 > 0 ; :: thesis: verum