let y be real number ; :: thesis: ( 1 <= y implies y + (sqrt ((y ^2 ) - 1)) > 0 )
assume A1: 1 <= y ; :: thesis: y + (sqrt ((y ^2 ) - 1)) > 0
then 0 <= (y ^2 ) - 1 by Lm4;
then 0 <= sqrt ((y ^2 ) - 1) by SQUARE_1:def 4;
then 0 + y <= (sqrt ((y ^2 ) - 1)) + y by XREAL_1:9;
hence y + (sqrt ((y ^2 ) - 1)) > 0 by A1; :: thesis: verum