theorem Th182: :: XCMPLX_1:182

for a being Complex holds
( not a * a = 1 or a = 1 or a = - 1 )