let x, y be real number ; :: thesis: ( x ^2 < 1 & y ^2 < 1 implies x * y <> - 1 )
assume A1: ( x ^2 < 1 & y ^2 < 1 ) ; :: thesis: x * y <> - 1
assume x * y = - 1 ; :: thesis: contradiction
then (x * y) * (x * y) = 1 ;
then (x * x) * (y * y) = 1 ;
hence contradiction by A1, Lm2; :: thesis: verum