theorem :: POLYEQ_3:20

for s, z being Complex st z ^2 = s & Im s = 0 & Re s > 0 & not z = sqrt (Re s) holds
z = - (sqrt (Re s))