let x, y be real number ; :: thesis: ((sqrt ((x ^2 ) + 1)) * (sqrt ((y ^2 ) + 1))) - (x * y) > 0
A1: ( (x ^2 ) + 1 > 0 & (y ^2 ) + 1 > 0 & sqrt ((x ^2 ) + 1) > 0 & sqrt ((y ^2 ) + 1) > 0 ) by Lm8, Th4;
then A2: (sqrt ((x ^2 ) + 1)) * (sqrt ((y ^2 ) + 1)) > 0 * (sqrt ((y ^2 ) + 1)) by XREAL_1:70;
A3: ( 0 <= x ^2 & 0 <= y ^2 ) by XREAL_1:65;
A4: 0 + 1 <= ((x ^2 ) + (y ^2 )) + 1 by A3, XREAL_1:8;
assume ((sqrt ((x ^2 ) + 1)) * (sqrt ((y ^2 ) + 1))) - (x * y) <= 0 ; :: thesis: contradiction
then ((sqrt ((x ^2 ) + 1)) * (sqrt ((y ^2 ) + 1))) - (x * y) <= 0 ;
then (sqrt ((x ^2 ) + 1)) * (sqrt ((y ^2 ) + 1)) <= x * y by XREAL_1:52;
then ((sqrt ((x ^2 ) + 1)) * (sqrt ((y ^2 ) + 1))) ^2 <= (x * y) ^2 by A2, SQUARE_1:77;
then ((sqrt ((x ^2 ) + 1)) ^2 ) * ((sqrt ((y ^2 ) + 1)) ^2 ) <= (x * y) ^2 ;
then ((x ^2 ) + 1) * ((sqrt ((y ^2 ) + 1)) ^2 ) <= (x * y) ^2 by A1, SQUARE_1:def 4;
then ((x ^2 ) + 1) * ((y ^2 ) + 1) <= (x * y) ^2 by A1, SQUARE_1:def 4;
then (((((x * y) ^2 ) + (x ^2 )) + (y ^2 )) + 1) - ((x * y) ^2 ) <= ((x * y) ^2 ) - ((x * y) ^2 ) by XREAL_1:15;
hence contradiction by A4; :: thesis: verum