let a, y be Real; :: thesis: ( not y ^2 = a or y = sqrt a or y = - (sqrt a) )
assume A1: y ^2 = a ; :: thesis: ( y = sqrt a or y = - (sqrt a) )
then A2: a >= 0 by XREAL_1:63;
Polynom (1,0,(- a),y) = 0 by A1;
then ( y = ((- 0) + (sqrt (delta (1,0,(- a))))) / (2 * 1) or y = ((- 0) - (sqrt (delta (1,0,(- a))))) / (2 * 1) ) by A2, POLYEQ_1:5;
then ( y = (sqrt (4 * a)) / 2 or y = (0 - (sqrt (4 * a))) / 2 ) ;
then ( y = ((sqrt a) * 2) / 2 or y = (- (2 * (sqrt a))) / 2 ) by A2, SQUARE_1:20, SQUARE_1:29;
hence ( y = sqrt a or y = - (sqrt a) ) ; :: thesis: verum