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