let t be real number ; :: 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:77;
then (t ^2 ) - (t ^2 ) <= 1 - (t ^2 ) by XREAL_1:15;
hence 0 <= 1 - (t ^2 ) ; :: thesis: verum