theorem Th73: :: COMPLEX2:75

for a, b being Complex st a <> 0 & b <> 0 holds
( Re (a .|. b) = 0 iff ( angle (a,0,b) = PI / 2 or angle (a,0,b) = (3 / 2) * PI ) )