let t be real number ; :: thesis: ( 0 < t implies 0 < (1 + (sqrt (1 + (t ^2 )))) / t )
assume A1: 0 < t ; :: thesis: 0 < (1 + (sqrt (1 + (t ^2 )))) / t
0 + 1 < (sqrt (1 + (t ^2 ))) + 1 by Th4, XREAL_1:10;
then 0 / t < (1 + (sqrt (1 + (t ^2 )))) / t by A1, XREAL_1:76;
hence 0 < (1 + (sqrt (1 + (t ^2 )))) / t ; :: thesis: verum