let t be Real; :: thesis: ((t ^2) - 1) / ((t ^2) + 1) < 1
A1: 0 < (t ^2) + 1 by Lm6;
(- 1) + (t ^2) < 1 + (t ^2) by XREAL_1:8;
then ((- 1) + (t ^2)) / (1 + (t ^2)) < (1 + (t ^2)) / (1 + (t ^2)) by A1, XREAL_1:74;
hence ((t ^2) - 1) / ((t ^2) + 1) < 1 by A1, XCMPLX_1:60; :: thesis: verum