let t be real number ; :: thesis: ( 0 < t & t <> 1 implies (2 * t) / ((t ^2 ) - 1) <> 0 )
assume A1: ( 0 < t & t <> 1 ) ; :: thesis: (2 * t) / ((t ^2 ) - 1) <> 0

per cases ( 1 < t or t < 1 ) by A1, XXREAL_0:1;

suppose A2: 1 < t ; :: thesis: (2 * t) / ((t ^2 ) - 1) <> 0

then t < t ^2 by SQUARE_1:76;
then 1 < t ^2 by A2, XXREAL_0:2;
then A3: 1 - 1 < (t ^2 ) - 1 by XREAL_1:16;
2 * 1 < 2 * t by A2, XREAL_1:70;
then 0 / ((t ^2 ) - 1) < (2 * t) / ((t ^2 ) - 1) by A3, XREAL_1:76;
hence (2 * t) / ((t ^2 ) - 1) <> 0 ; :: thesis: verum

end;

suppose A4: t < 1 ; :: thesis: (2 * t) / ((t ^2 ) - 1) <> 0

then t ^2 < t by A1, SQUARE_1:75;
then t ^2 < 1 by A4, XXREAL_0:2;
then A5: (t ^2 ) - 1 < 1 - 1 by XREAL_1:16;
0 * 2 < 2 * t by A1, XREAL_1:70;
then (2 * t) / ((t ^2 ) - 1) < 0 / ((t ^2 ) - 1) by A5, XREAL_1:77;
hence (2 * t) / ((t ^2 ) - 1) <> 0 ; :: thesis: verum

end;

end;