theorem :: COMPLEX1:42

for z being Complex holds
( Re (z - (z *')) = 0 & Im (z - (z *')) = 2 * (Im z) )