let b, c, d, x be real number ; :: 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