let x be Real; :: thesis: (x / (sqrt ((x ^2) + 1))) ^2 < 1
A1: x ^2 < (x ^2) + 1 by XREAL_1:29;
A2: x ^2 >= 0 by XREAL_1:63;
then (sqrt ((x ^2) + 1)) ^2 = sqrt (((x ^2) + 1) ^2) by SQUARE_1:29
.= (x ^2) + 1 by A2, SQUARE_1:22 ;
then A3: (x / (sqrt ((x ^2) + 1))) ^2 = (x ^2) / ((x ^2) + 1) by XCMPLX_1:76;

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

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

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

end;

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

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

end;

end;