theorem Th28: :: SIN_COS7:28

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