theorem Th23: :: COMPLEX1:23

for z being Complex st Re z = 0 & Im z <> 0 holds
( Re (z ") = 0 & Im (z ") = - ((Im z) ") )