let t be Real; :: 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 ;
then 0 * 2 < 2 * (t ^2) ;
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