let x, y be Real; :: thesis: ( y >= 0 & x >= 1 implies ((x ^2) - 1) / y >= 0 )
assume that
A1: y >= 0 and
A2: x >= 1 ; :: thesis: ((x ^2) - 1) / y >= 0
(x ^2) - 1 >= 0 by A2, Lm3;
hence ((x ^2) - 1) / y >= 0 by A1; :: thesis: verum