theorem :: POLYEQ_1:17

for a, b, c, d, y being Real st (((y |^ 3) + (0 * (y ^2))) + (((((3 * a) * c) - (b ^2)) / (3 * (a ^2))) * y)) + ((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))) = 0 holds
for p, q being Real st p = (((3 * a) * c) - (b ^2)) / (3 * (a ^2)) & q = (2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2))) holds
Polynom (1,0,p,q,y) = 0 ;