let t be real number ; :: thesis: ( 0 < t implies - 1 < ((t ^2 ) - 1) / ((t ^2 ) + 1) )
A1: 0 < (t ^2 ) + 1 by Lm8;
assume 0 < t ; :: thesis: - 1 < ((t ^2 ) - 1) / ((t ^2 ) + 1)
then 0 < t ^2 by SQUARE_1:74;
then 0 * 2 < 2 * (t ^2 ) by XREAL_1:70;
then 0 - ((t ^2 ) + 1) < (2 * (t ^2 )) - ((t ^2 ) + 1) by XREAL_1:16;
then (- ((t ^2 ) + 1)) / ((t ^2 ) + 1) < ((t ^2 ) - 1) / ((t ^2 ) + 1) by A1, XREAL_1:76;
then - (((t ^2 ) + 1) / ((t ^2 ) + 1)) < ((t ^2 ) - 1) / ((t ^2 ) + 1) ;
hence - 1 < ((t ^2 ) - 1) / ((t ^2 ) + 1) by A1, XCMPLX_1:60; :: thesis: verum