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