let t be real number ; :: thesis: ( 0 < t implies - 1 < ((t ^2) - 1) / ((t ^2) + 1) )
A1: 0 < (t ^2) + 1 by Lm6;
assume 0 < t ; :: thesis: - 1 < ((t ^2) - 1) / ((t ^2) + 1)
then 0 < t ^2 by SQUARE_1:12;
then 0 * 2 < 2 * (t ^2) by XREAL_1:68;
then 0 - ((t ^2) + 1) < (2 * (t ^2)) - ((t ^2) + 1) by XREAL_1:14;
then (- ((t ^2) + 1)) / ((t ^2) + 1) < ((t ^2) - 1) / ((t ^2) + 1) by A1, XREAL_1:74;
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