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 that
A1: x + y = p and
A2: x * y = q and
A3: (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 ) )
A4: delta (1,(- p),q) = ((- p) ^2) - ((4 * 1) * q) by QUIN_1:def 1
.= (p ^2) - (4 * q) ;
((1 * (y ^2)) + ((- p) * y)) + q = 0 by A1, A2;
then Polynom (1,(- p),q,y) = 0 by POLYEQ_1:def 2;
then A5: ( y = ((- (- p)) + (sqrt (delta (1,(- p),q)))) / (2 * 1) or y = ((- (- p)) - (sqrt (delta (1,(- p),q)))) / (2 * 1) ) by A3, A4, POLYEQ_1:5;

now :: 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 ) )

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

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 * 2) / 2) - ((p / 2) + ((sqrt (delta (1,(- p),q))) / 2)) by A1
.= ((p * 2) / 2) - ((p / 2) + ((sqrt ((p ^2) - (4 * q))) / 2)) by A4 ;
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 A4, A6; :: thesis: verum

end;

suppose A7: 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 A4 ;
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 A4, A7; :: 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