let t be real number ; :: 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:10;
then (1 + (sqrt (1 + (t ^2 )))) / t < 0 / t by A1, XREAL_1:77;
hence (1 + (sqrt (1 + (t ^2 )))) / t < 0 ; :: thesis: verum