theorem :: POLYEQ_4:21

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