theorem Th2: :: POLYNOM9:2

for z1, z2 being Complex st Re z1 >= 0 & Re z2 >= 0 & Im z1 >= 0 & Im z2 >= 0 & z1 ^2 = z2 ^2 & z1 ^2 is Real holds
z1 = z2