let x be Real; :: thesis: (sqrt ((x ^2) + 1)) + x > 0

per cases ( x > 0 or x <= 0 ) ;

suppose x > 0 ; :: thesis: (sqrt ((x ^2) + 1)) + x > 0

hence (sqrt ((x ^2) + 1)) + x > 0 by Th4, XREAL_1:29; :: thesis: verum

end;

suppose A1: x <= 0 ; :: thesis: (sqrt ((x ^2) + 1)) + x > 0

x ^2 < (x ^2) + 1 by XREAL_1:29;
then sqrt (x ^2) < sqrt ((x ^2) + 1) by SQUARE_1:27, XREAL_1:63;
then - x < sqrt ((x ^2) + 1) by A1, SQUARE_1:23;
hence (sqrt ((x ^2) + 1)) + x > 0 by XREAL_1:62; :: thesis: verum

end;

end;