let x, y, p, q be Real; :: thesis: ( x + y = p & x * y = q & (p ^2 ) - (4 * q) >= 0 & not ( x = (p + (sqrt ((p ^2 ) - (4 * q)))) / 2 & y = (p - (sqrt ((p ^2 ) - (4 * q)))) / 2 ) implies ( x = (p - (sqrt ((p ^2 ) - (4 * q)))) / 2 & y = (p + (sqrt ((p ^2 ) - (4 * q)))) / 2 ) )
assume A1: ( x + y = p & x * y = q & (p ^2 ) - (4 * q) >= 0 ) ; :: thesis: ( ( x = (p + (sqrt ((p ^2 ) - (4 * q)))) / 2 & y = (p - (sqrt ((p ^2 ) - (4 * q)))) / 2 ) or ( x = (p - (sqrt ((p ^2 ) - (4 * q)))) / 2 & y = (p + (sqrt ((p ^2 ) - (4 * q)))) / 2 ) )
then ((1 * (y ^2 )) + ((- p) * y)) + q = 0 ;
then A2: Polynom 1,(- p),q,y = 0 by POLYEQ_1:def 2;
A3: delta 1,(- p),q = ((- p) ^2 ) - ((4 * 1) * q) by QUIN_1:def 1
.= (p ^2 ) - (4 * q) ;
then A4: ( y = ((- (- p)) + (sqrt (delta 1,(- p),q))) / (2 * 1) or y = ((- (- p)) - (sqrt (delta 1,(- p),q))) / (2 * 1) ) by A1, A2, POLYEQ_1:5;

now

per cases ( y = (p + (sqrt (delta 1,(- p),q))) / 2 or y = (p - (sqrt (delta 1,(- p),q))) / 2 ) by A4;

suppose A5: y = (p + (sqrt (delta 1,(- p),q))) / 2 ; :: thesis: ( ( x = (p + (sqrt ((p ^2 ) - (4 * q)))) / 2 & y = (p - (sqrt ((p ^2 ) - (4 * q)))) / 2 ) or ( x = (p - (sqrt ((p ^2 ) - (4 * q)))) / 2 & y = (p + (sqrt ((p ^2 ) - (4 * q)))) / 2 ) )

then x = ((p * 2) / 2) - ((p / 2) + ((sqrt (delta 1,(- p),q)) / 2)) by A1
.= ((p * 2) / 2) - ((p / 2) + ((sqrt ((p ^2 ) - (4 * q))) / 2)) by A3 ;
hence ( ( x = (p + (sqrt ((p ^2 ) - (4 * q)))) / 2 & y = (p - (sqrt ((p ^2 ) - (4 * q)))) / 2 ) or ( x = (p - (sqrt ((p ^2 ) - (4 * q)))) / 2 & y = (p + (sqrt ((p ^2 ) - (4 * q)))) / 2 ) ) by A3, A5; :: thesis: verum

end;

suppose A6: y = (p - (sqrt (delta 1,(- p),q))) / 2 ; :: thesis: ( ( x = (p + (sqrt ((p ^2 ) - (4 * q)))) / 2 & y = (p - (sqrt ((p ^2 ) - (4 * q)))) / 2 ) or ( x = (p - (sqrt ((p ^2 ) - (4 * q)))) / 2 & y = (p + (sqrt ((p ^2 ) - (4 * q)))) / 2 ) )

then x = p - (((p - (sqrt (delta 1,(- p),q))) + 0 ) / 2) by A1
.= p - (((p - (sqrt ((p ^2 ) - (4 * q)))) + 0 ) / 2) by A3 ;
hence ( ( x = (p + (sqrt ((p ^2 ) - (4 * q)))) / 2 & y = (p - (sqrt ((p ^2 ) - (4 * q)))) / 2 ) or ( x = (p - (sqrt ((p ^2 ) - (4 * q)))) / 2 & y = (p + (sqrt ((p ^2 ) - (4 * q)))) / 2 ) ) by A3, A6; :: thesis: verum

end;

end;

end;

hence ( ( x = (p + (sqrt ((p ^2 ) - (4 * q)))) / 2 & y = (p - (sqrt ((p ^2 ) - (4 * q)))) / 2 ) or ( x = (p - (sqrt ((p ^2 ) - (4 * q)))) / 2 & y = (p + (sqrt ((p ^2 ) - (4 * q)))) / 2 ) ) ; :: thesis: verum