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