let x be Real; :: 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:8;
then sqrt ((x ^2) + 1) > sqrt (x ^2) by SQUARE_1:27, XREAL_1:63;
hence sqrt ((x ^2) + 1) > x by A1, SQUARE_1:22; :: thesis: verum

end;

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

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

end;

end;