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