let t be real number ; :: thesis: ( 0 < t implies 0 < (2 * t) / (1 + (t ^2)) )
assume 0 < t ; :: thesis: 0 < (2 * t) / (1 + (t ^2))
then A1: 0 * 2 < 2 * t by XREAL_1:68;
(t ^2) + 1 > 0 by Lm6;
then 0 / ((t ^2) + 1) < (2 * t) / ((t ^2) + 1) by A1, XREAL_1:74;
hence 0 < (2 * t) / (1 + (t ^2)) ; :: thesis: verum