let x be Complex; :: thesis: ( not x ^2 = 1 or x = 1 or x = - 1 )
assume x ^2 = 1 ; :: thesis: ( x = 1 or x = - 1 )
then (x - 1) * (x + 1) = 0 ;
then ( x - 1 = 0 or x + 1 = 0 ) ;
hence ( x = 1 or x = - 1 ) ; :: thesis: verum