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