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