theorem :: POLYEQ_1:23

for a, c, x being Real st a <> 0 & c / a < 0 & Polynom (a,0,c,0,x) = 0 & not x = 0 & not x = sqrt (- (c / a)) holds
x = - (sqrt (- (c / a)))