let t be Real; :: thesis: ( 0 < t & t <= 1 implies 0 <= 1 - (t ^2) )
assume ( 0 < t & t <= 1 ) ; :: thesis: 0 <= 1 - (t ^2)
then t ^2 <= 1 ^2 by SQUARE_1:15;
then (t ^2) - (t ^2) <= 1 - (t ^2) by XREAL_1:13;
hence 0 <= 1 - (t ^2) ; :: thesis: verum