let x, y be Real; :: thesis: ((sqrt ((x ^2) + 1)) * (sqrt ((y ^2) + 1))) - (x * y) > 0
A1: (y ^2) + 1 > 0 by Lm6;
assume ((sqrt ((x ^2) + 1)) * (sqrt ((y ^2) + 1))) - (x * y) <= 0 ; :: thesis: contradiction
then A2: (sqrt ((x ^2) + 1)) * (sqrt ((y ^2) + 1)) <= x * y by XREAL_1:50;
( sqrt ((x ^2) + 1) > 0 & sqrt ((y ^2) + 1) > 0 ) by Th4;
then ((sqrt ((x ^2) + 1)) * (sqrt ((y ^2) + 1))) ^2 <= (x * y) ^2 by A2, SQUARE_1:15;
then A3: ((sqrt ((x ^2) + 1)) ^2) * ((sqrt ((y ^2) + 1)) ^2) <= (x * y) ^2 ;
(x ^2) + 1 > 0 by Lm6;
then ((x ^2) + 1) * ((sqrt ((y ^2) + 1)) ^2) <= (x * y) ^2 by A3, SQUARE_1:def 2;
then ((x ^2) + 1) * ((y ^2) + 1) <= (x * y) ^2 by A1, SQUARE_1:def 2;
then A4: (((((x * y) ^2) + (x ^2)) + (y ^2)) + 1) - ((x * y) ^2) <= ((x * y) ^2) - ((x * y) ^2) by XREAL_1:13;
( 0 <= x ^2 & 0 <= y ^2 ) by XREAL_1:63;
then 0 + 1 <= ((x ^2) + (y ^2)) + 1 by XREAL_1:6;
hence contradiction by A4; :: thesis: verum