let t be Real; :: 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 Lm16;
then 0 * 4 <= 4 * (1 - (t ^2)) ;
hence 0 <= 4 - (4 * (t ^2)) ; :: thesis: verum