let y be Real; :: 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 Lm3;
then 0 <= sqrt ((y ^2) - 1) by SQUARE_1:def 2;
hence y + (sqrt ((y ^2) - 1)) > 0 by A1; :: thesis: verum