theorem Th20: :: COMPLSP2:24

for z being Complex holds z + (z *') = 2 * (Re z)