let t be real number ; :: thesis: ( 0 < t implies (2 * t) / (1 + (t ^2 )) <= 1 )
assume 0 < t ; :: thesis: (2 * t) / (1 + (t ^2 )) <= 1
then A1: 0 * 2 < 2 * t by XREAL_1:70;
0 <= (t - 1) ^2 by XREAL_1:65;
then 0 + (2 * t) <= (((t ^2 ) - (2 * t)) + 1) + (2 * t) by XREAL_1:8;
hence (2 * t) / (1 + (t ^2 )) <= 1 by A1, XREAL_1:185; :: thesis: verum