let t be Real; :: thesis: ( 0 < t & t <= 1 implies 0 < 1 + (sqrt (1 - (t ^2))) )
assume ( 0 < t & t <= 1 ) ; :: thesis: 0 < 1 + (sqrt (1 - (t ^2)))
then 0 <= 1 - (t ^2) by Lm16;
then 0 <= sqrt (1 - (t ^2)) by SQUARE_1:17, SQUARE_1:26;
hence 0 < 1 + (sqrt (1 - (t ^2))) ; :: thesis: verum