let x be Complex; :: thesis: ( x .|. x = 0 implies x = 0 )
assume x .|. x = 0 ; :: thesis: x = 0
then ((Re x) ^2) + ((Im x) ^2) = 0 by Th28;
hence x = 0 by COMPLEX1:5; :: thesis: verum