theorem Th19: :: POLYEQ_3:19

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