theorem Th14: :: POLYEQ_4:14

for x, y, p, q being Real st 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 ) holds
( x = (p - (sqrt ((p ^2) - (4 * q)))) / 2 & y = (p + (sqrt ((p ^2) - (4 * q)))) / 2 )