theorem :: COMPLEX1:26

for z1, z2 being Complex st Re z1 = 0 & Re z2 = 0 & Im z2 <> 0 holds
( Re (z1 / z2) = (Im z1) / (Im z2) & Im (z1 / z2) = 0 )