let x, y be Real; ( 1 <= x & 1 <= y implies 0 <= (x * (sqrt ((y ^2) - 1))) + (y * (sqrt ((x ^2) - 1))) )
assume that
A1:
1 <= x
and
A2:
1 <= y
; 0 <= (x * (sqrt ((y ^2) - 1))) + (y * (sqrt ((x ^2) - 1)))
0 <= (y ^2) - 1
by A2, Lm3;
then A3:
0 <= sqrt ((y ^2) - 1)
by SQUARE_1:def 2;
0 <= (x ^2) - 1
by A1, Lm3;
then
0 <= sqrt ((x ^2) - 1)
by SQUARE_1:def 2;
hence
0 <= (x * (sqrt ((y ^2) - 1))) + (y * (sqrt ((x ^2) - 1)))
by A1, A2, A3; verum