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