theorem :: COMPLEX2:33

for x being Complex st x .|. x = 0 holds
x = 0