let a, b be Complex; :: thesis: ( not a ^2 = b ^2 or a = b or a = - b )
assume a ^2 = b ^2 ; :: thesis: ( a = b or a = - b )
then (a + b) * (a - b) = 0 ;
then ( a + b = 0 or a - b = 0 ) by XCMPLX_1:6;
hence ( a = b or a = - b ) ; :: thesis: verum