let t be Real; :: thesis: ( ( 1 < t or t < - 1 ) implies 0 < (t + 1) / (t - 1) )
assume A1: ( 1 < t or t < - 1 ) ; :: thesis: 0 < (t + 1) / (t - 1)

per cases ( 1 < t or t < - 1 ) by A1;

suppose A2: 1 < t ; :: thesis: 0 < (t + 1) / (t - 1)

then 1 - 1 < t - 1 by XREAL_1:14;
then 0 / (t - 1) < (t + 1) / (t - 1) by A2;
hence 0 < (t + 1) / (t - 1) ; :: thesis: verum

end;

suppose A3: t < - 1 ; :: thesis: 0 < (t + 1) / (t - 1)

then t + 1 < (- 1) + 1 by XREAL_1:8;
then 0 / (t - 1) < (t + 1) / (t - 1) by A3;
hence 0 < (t + 1) / (t - 1) ; :: thesis: verum

end;

end;