theorem Th22: :: COMPLEX1:22
for z being Complex st Re z <> 0 & Im z = 0 holds
( Re (z ") = (Re z) " & Im (z ") = 0 )