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:70;
(t ^2 ) + 1 > 0 by Lm8;
then 0 / ((t ^2 ) + 1) < (2 * t) / ((t ^2 ) + 1) by A1, XREAL_1:76;
hence 0 < (2 * t) / (1 + (t ^2 )) ; :: thesis: verum