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