let x be Real; :: thesis: ( 1 <= x implies 0 < x + (sqrt ((x ^2) - 1)) )
assume A1: 1 <= x ; :: thesis: 0 < x + (sqrt ((x ^2) - 1))
then (x ^2) - 1 >= 0 by Lm3;
then 0 <= sqrt ((x ^2) - 1) by SQUARE_1:def 2;
hence 0 < x + (sqrt ((x ^2) - 1)) by A1; :: thesis: verum