let x be real number ; :: 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:31; :: thesis: verum

end;

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

x ^2 < (x ^2 ) + 1 by XREAL_1:31;
then sqrt (x ^2 ) < sqrt ((x ^2 ) + 1) by SQUARE_1:95, XREAL_1:65;
then - x < sqrt ((x ^2 ) + 1) by A1, SQUARE_1:90;
hence (sqrt ((x ^2 ) + 1)) + x > 0 by XREAL_1:64; :: thesis: verum

end;

end;