let t be Real; :: thesis: ( 0 < t implies (2 * t) / (1 + (t ^2)) <= 1 )
0 <= (t - 1) ^2 by XREAL_1:63;
then A1: 0 + (2 * t) <= (((t ^2) - (2 * t)) + 1) + (2 * t) by XREAL_1:6;
assume 0 < t ; :: thesis: (2 * t) / (1 + (t ^2)) <= 1
hence (2 * t) / (1 + (t ^2)) <= 1 by A1, XREAL_1:183; :: thesis: verum