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