let x be Element of COMPLEX ; :: thesis: ( x .|. x = 0 implies x = 0 )
assume x .|. x = 0 ; :: thesis: x = 0
then ((Re x) ^2 ) + ((Im x) ^2 ) = 0 by Th43;
hence x = 0 by COMPLEX1:13; :: thesis: verum