theorem :: COMPLEX1:25

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