theorem Th4: :: POLYEQ_4:4

for x, a being Real
for n being Element of NAT st a > 0 & n is even & n >= 1 & x |^ n = a & not x = n -root a holds
x = - (n -root a)