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