let x, y be real number ; :: 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:52;
( 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:77;
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 4;
then ((x ^2 ) + 1) * ((y ^2 ) + 1) <= (x * y) ^2 by A1, SQUARE_1:def 4;
then A4: (((((x * y) ^2 ) + (x ^2 )) + (y ^2 )) + 1) - ((x * y) ^2 ) <= ((x * y) ^2 ) - ((x * y) ^2 ) by XREAL_1:15;
( 0 <= x ^2 & 0 <= y ^2 ) by XREAL_1:65;
then 0 + 1 <= ((x ^2 ) + (y ^2 )) + 1 by XREAL_1:8;
hence contradiction by A4; :: thesis: verum