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