theorem Th12: :: POLYEQ_3:12

for a, y being Real holds
( not y ^2 = a or y = sqrt a or y = - (sqrt a) )