let t be real number ; :: 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 Lm19;
then 0 <= sqrt (1 - (t ^2 )) by SQUARE_1:82, SQUARE_1:94;
then 0 + 1 <= (sqrt (1 - (t ^2 ))) + 1 by XREAL_1:8;
hence 0 < 1 + (sqrt (1 - (t ^2 ))) ; :: thesis: verum