let t be real number ; :: thesis: ( - 1 < t & t < 1 implies 0 < (t + 1) / (1 - t) )
assume ( - 1 < t & t < 1 ) ; :: thesis: 0 < (t + 1) / (1 - t)
then ( (- 1) + 1 < t + 1 & t - t < 1 - t ) by XREAL_1:8;
then 0 / (1 - t) < (t + 1) / (1 - t) by XREAL_1:74;
hence 0 < (t + 1) / (1 - t) ; :: thesis: verum