let y, x be real number ; :: thesis: ( y >= 0 & x >= 1 implies ((x ^2 ) - 1) / y >= 0 )
assume A1: ( y >= 0 & x >= 1 ) ; :: thesis: ((x ^2 ) - 1) / y >= 0
then (x ^2 ) - 1 >= 0 by Lm4;
hence ((x ^2 ) - 1) / y >= 0 by A1; :: thesis: verum