let t be real number ; :: thesis: ( 0 < t & t <= 1 implies 0 <= 4 - (4 * (t ^2 )) )
assume ( 0 < t & t <= 1 ) ; :: thesis: 0 <= 4 - (4 * (t ^2 ))
then 0 <= 1 - (t ^2 ) by Lm19;
then 0 * 4 <= 4 * (1 - (t ^2 )) ;
hence 0 <= 4 - (4 * (t ^2 )) ; :: thesis: verum