let a, b, x 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 A1: ( a <> 0 & ((b ^2 ) - ((2 * a) * b)) - (3 * (a ^2 )) >= 0 & 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) )
then (((a * (x |^ 3)) + (b * (x ^2 ))) + (b * x)) + a = 0 by 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 by POWER:31;
then (((x |^ 3) + (1 |^ 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 A2: (((((x ^2 ) * a) - (x * a)) + (x * b)) + a) * (x + 1) = 0 ;

now

per cases ( x + 1 = 0 or ((a * (x ^2 )) - ((a - b) * x)) + a = 0 ) by A2, XCMPLX_1:6;

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 ((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) )

then ((a * (x ^2 )) + (((- a) + b) * x)) + a = 0 ;
then A3: Polynom a,((- a) + b),a,x = 0 by POLYEQ_1:def 2;
A4: 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 )) ;
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, A3, 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 A4; :: 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