theorem Th27: :: SIN_COS7:27

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