let x, y be real number ; :: thesis: ( 1 <= x & 1 <= y implies 0 <= (x * (sqrt ((y ^2 ) - 1))) + (y * (sqrt ((x ^2 ) - 1))) )
assume A1: ( 1 <= x & 1 <= y ) ; :: thesis: 0 <= (x * (sqrt ((y ^2 ) - 1))) + (y * (sqrt ((x ^2 ) - 1)))
then ( 0 <= (x ^2 ) - 1 & 0 <= (y ^2 ) - 1 ) by Lm4;
then ( 0 <= sqrt ((x ^2 ) - 1) & 0 <= sqrt ((y ^2 ) - 1) ) by SQUARE_1:def 4;
then A2: ( 0 * y <= (sqrt ((x ^2 ) - 1)) * y & 0 * x <= (sqrt ((y ^2 ) - 1)) * x ) by A1;
thus 0 <= (x * (sqrt ((y ^2 ) - 1))) + (y * (sqrt ((x ^2 ) - 1))) by A2; :: thesis: verum