let x be Real; :: thesis: ( x <> 1 implies (1 - x) ^2 > 0 )
assume x <> 1 ; :: thesis: (1 - x) ^2 > 0
then 0 <> 1 - x ;
hence (1 - x) ^2 > 0 by SQUARE_1:12; :: thesis: verum