theorem Th12: :: SIN_COS7:12

for x being Real st x <> 1 holds
(1 - x) ^2 > 0