let t be Real; :: 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;
hence 0 < (1 + (sqrt (1 - (t ^2)))) / t ; :: thesis: verum