let x be real number ; :: thesis: (x / (sqrt ((x ^2 ) + 1))) ^2 < 1
x ^2 >= 0 by XREAL_1:65;
then A1: (x ^2 ) + 1 >= 0 + 1 by XREAL_1:9;
A2: x ^2 < (x ^2 ) + 1 by XREAL_1:31;
(sqrt ((x ^2 ) + 1)) ^2 = sqrt (((x ^2 ) + 1) ^2 ) by A1, SQUARE_1:97
.= (x ^2 ) + 1 by A1, SQUARE_1:89 ;
then A3: (x / (sqrt ((x ^2 ) + 1))) ^2 = (x ^2 ) / ((x ^2 ) + 1) by XCMPLX_1:77;

per cases ( x ^2 > 0 or x ^2 = 0 ) by XREAL_1:65;

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

hence (x / (sqrt ((x ^2 ) + 1))) ^2 < 1 by A2, A3, XREAL_1:191; :: thesis: verum

end;

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

hence (x / (sqrt ((x ^2 ) + 1))) ^2 < 1 by A3; :: thesis: verum

end;

end;