theorem :: XCMPLX_1:223

for a being Complex st a <> 0 & a = a " & not a = 1 holds
a = - 1 by Lm18;