for x, y being Real st x ^2 < 1 & y ^2 < 1 holds
x * y <> 1