theorem Th18: :: POLYEQ_1:18

for p, q, y being Real st Polynom (1,0,p,q,y) = 0 holds
for u, v being Real st y = u + v & ((3 * v) * u) + p = 0 holds
( (u |^ 3) + (v |^ 3) = - q & (u |^ 3) * (v |^ 3) = (- (p / 3)) |^ 3 )