let x, a, b be Real; :: thesis: ( a <> 0 & ((b ^2) - ((2 * a) * b)) - (3 * (a ^2)) >= 0 & Polynom (a,b,b,a,x) = 0 & not x = - 1 & not x = ((a - b) + (sqrt (((b ^2) - ((2 * a) * b)) - (3 * (a ^2))))) / (2 * a) implies x = ((a - b) - (sqrt (((b ^2) - ((2 * a) * b)) - (3 * (a ^2))))) / (2 * a) )
assume that
A1: ( a <> 0 & ((b ^2) - ((2 * a) * b)) - (3 * (a ^2)) >= 0 ) and
A2: Polynom (a,b,b,a,x) = 0 ; :: thesis: ( x = - 1 or x = ((a - b) + (sqrt (((b ^2) - ((2 * a) * b)) - (3 * (a ^2))))) / (2 * a) or x = ((a - b) - (sqrt (((b ^2) - ((2 * a) * b)) - (3 * (a ^2))))) / (2 * a) )
(((a * (x |^ 3)) + (b * (x ^2))) + (b * x)) + a = 0 by A2, POLYEQ_1:def 4;
then (((x |^ 3) + 1) * a) + ((((x ^2) + x) + 0) * b) = 0 ;
then (((x |^ 3) + (1 to_power 3)) * a) + (((x + 1) * x) * b) = 0 ;
then (((x + 1) * (((x ^2) - (x * 1)) + (1 ^2))) * a) + (((x + 1) * x) * b) = 0 by Th11;
then A3: (((((x ^2) * a) - (x * a)) + (x * b)) + a) * (x + 1) = 0 ;

now :: thesis: ( ( x + 1 = 0 & ( x = - 1 or x = ((a - b) + (sqrt (((b ^2) - ((2 * a) * b)) - (3 * (a ^2))))) / (2 * a) or x = ((a - b) - (sqrt (((b ^2) - ((2 * a) * b)) - (3 * (a ^2))))) / (2 * a) ) ) or ( ((a * (x ^2)) - ((a - b) * x)) + a = 0 & ( x = - 1 or x = ((a - b) + (sqrt (((b ^2) - ((2 * a) * b)) - (3 * (a ^2))))) / (2 * a) or x = ((a - b) - (sqrt (((b ^2) - ((2 * a) * b)) - (3 * (a ^2))))) / (2 * a) ) ) )

per cases ( x + 1 = 0 or ((a * (x ^2)) - ((a - b) * x)) + a = 0 ) by A3;

case x + 1 = 0 ; :: thesis: ( x = - 1 or x = ((a - b) + (sqrt (((b ^2) - ((2 * a) * b)) - (3 * (a ^2))))) / (2 * a) or x = ((a - b) - (sqrt (((b ^2) - ((2 * a) * b)) - (3 * (a ^2))))) / (2 * a) )

hence ( x = - 1 or x = ((a - b) + (sqrt (((b ^2) - ((2 * a) * b)) - (3 * (a ^2))))) / (2 * a) or x = ((a - b) - (sqrt (((b ^2) - ((2 * a) * b)) - (3 * (a ^2))))) / (2 * a) ) ; :: thesis: verum

end;

case A4: ((a * (x ^2)) - ((a - b) * x)) + a = 0 ; :: thesis: ( x = - 1 or x = ((a - b) + (sqrt (((b ^2) - ((2 * a) * b)) - (3 * (a ^2))))) / (2 * a) or x = ((a - b) - (sqrt (((b ^2) - ((2 * a) * b)) - (3 * (a ^2))))) / (2 * a) )

A5: delta (a,((- a) + b),a) = (((- a) + b) ^2) - ((4 * a) * a) by QUIN_1:def 1
.= ((b ^2) - ((2 * a) * b)) + ((- (4 - 1)) * (a ^2)) ;
((a * (x ^2)) + (((- a) + b) * x)) + a = 0 by A4;
then Polynom (a,((- a) + b),a,x) = 0 by POLYEQ_1:def 2;
then ( x = ((- ((- a) + b)) + (sqrt (delta (a,((- a) + b),a)))) / (2 * a) or x = ((- ((- a) + b)) - (sqrt (delta (a,((- a) + b),a)))) / (2 * a) ) by A1, A5, POLYEQ_1:5;
hence ( x = - 1 or x = ((a - b) + (sqrt (((b ^2) - ((2 * a) * b)) - (3 * (a ^2))))) / (2 * a) or x = ((a - b) - (sqrt (((b ^2) - ((2 * a) * b)) - (3 * (a ^2))))) / (2 * a) ) by A5; :: thesis: verum

end;

end;

end;

hence ( x = - 1 or x = ((a - b) + (sqrt (((b ^2) - ((2 * a) * b)) - (3 * (a ^2))))) / (2 * a) or x = ((a - b) - (sqrt (((b ^2) - ((2 * a) * b)) - (3 * (a ^2))))) / (2 * a) ) ; :: thesis: verum