let b, c, d, x be Real; :: thesis: ( b <> 0 & delta (b,c,d) > 0 & Polynom (0,b,c,d,x) = 0 & not x = ((- c) + (sqrt (delta (b,c,d)))) / (2 * b) implies x = ((- c) - (sqrt (delta (b,c,d)))) / (2 * b) )
assume A1: ( b <> 0 & delta (b,c,d) > 0 ) ; :: thesis: ( not Polynom (0,b,c,d,x) = 0 or x = ((- c) + (sqrt (delta (b,c,d)))) / (2 * b) or x = ((- c) - (sqrt (delta (b,c,d)))) / (2 * b) )
assume Polynom (0,b,c,d,x) = 0 ; :: thesis: ( x = ((- c) + (sqrt (delta (b,c,d)))) / (2 * b) or x = ((- c) - (sqrt (delta (b,c,d)))) / (2 * b) )
then Polynom (b,c,d,x) = 0 ;
hence ( x = ((- c) + (sqrt (delta (b,c,d)))) / (2 * b) or x = ((- c) - (sqrt (delta (b,c,d)))) / (2 * b) ) by A1, Th5; :: thesis: verum