let x be real number ; :: thesis: sqrt ((x ^2 ) + 1) > x

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

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

(x ^2 ) + 1 > (x ^2 ) + 0 by XREAL_1:10;
then sqrt ((x ^2 ) + 1) > sqrt (x ^2 ) by SQUARE_1:95, XREAL_1:65;
hence sqrt ((x ^2 ) + 1) > x by A1, SQUARE_1:89; :: thesis: verum

end;

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

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

end;

end;