let t be Real; :: 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 XREAL_1:8;
then 1 < sqrt ((t ^2) + 1) by SQUARE_1:18, SQUARE_1:27;
then - (sqrt ((t ^2) + 1)) < - 1 by XREAL_1:24;
then (- (sqrt ((t ^2) + 1))) + 1 < (- 1) + 1 by XREAL_1:8;
then (1 - (sqrt ((t ^2) + 1))) / t < 0 / t by A1;
hence (1 - (sqrt (1 + (t ^2)))) / t < 0 ; :: thesis: verum