let t be Real; :: thesis: ( 0 < t & t <> 1 & not 1 < ((t ^2) + 1) / ((t ^2) - 1) implies ((t ^2) + 1) / ((t ^2) - 1) < - 1 )
assume that
A1: 0 < t and
A2: t <> 1 ; :: thesis: ( 1 < ((t ^2) + 1) / ((t ^2) - 1) or ((t ^2) + 1) / ((t ^2) - 1) < - 1 )
( 1 < t or t < 1 ) by A2, XXREAL_0:1;
then A3: ( 1 - 1 < t - 1 or t - 1 < 1 - 1 ) by XREAL_1:14;

per cases ( 0 < t - 1 or t - 1 < 0 ) by A3;

suppose 0 < t - 1 ; :: thesis: ( 1 < ((t ^2) + 1) / ((t ^2) - 1) or ((t ^2) + 1) / ((t ^2) - 1) < - 1 )

then A4: 0 + 1 < (t - 1) + 1 by XREAL_1:8;
then t < t ^2 by SQUARE_1:14;
then 1 < t ^2 by A4, XXREAL_0:2;
then A5: 1 - 1 < (t ^2) - 1 by XREAL_1:14;
(- 1) + (t ^2) < 1 + (t ^2) by XREAL_1:8;
hence ( 1 < ((t ^2) + 1) / ((t ^2) - 1) or ((t ^2) + 1) / ((t ^2) - 1) < - 1 ) by A5, XREAL_1:187; :: thesis: verum

end;

suppose t - 1 < 0 ; :: thesis: ( 1 < ((t ^2) + 1) / ((t ^2) - 1) or ((t ^2) + 1) / ((t ^2) - 1) < - 1 )

then A6: (t - 1) + 1 < 0 + 1 by XREAL_1:8;
then t ^2 < t by A1, SQUARE_1:13;
then t ^2 < 1 by A6, XXREAL_0:2;
then A7: (t ^2) - (t ^2) < 1 - (t ^2) by XREAL_1:14;
0 < t ^2 by A1;
then (- (t ^2)) + 1 < (t ^2) + 1 by XREAL_1:8;
then 1 < ((t ^2) + 1) / (1 - (t ^2)) by A7, XREAL_1:187;
then (- 1) * (((t ^2) + 1) / (1 - (t ^2))) < 1 * (- 1) by XREAL_1:69;
then (- ((t ^2) + 1)) / (1 - (t ^2)) < 1 * (- 1) ;
then ((t ^2) + 1) / (- (1 - (t ^2))) < 1 * (- 1) by XCMPLX_1:192;
hence ( 1 < ((t ^2) + 1) / ((t ^2) - 1) or ((t ^2) + 1) / ((t ^2) - 1) < - 1 ) ; :: thesis: verum

end;

end;