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