let a, b, c be Real; :: thesis: ( 0 <= a & c < 0 & delta (a,b,c) = 0 implies a = 0 )
assume that
A1: 0 <= a and
A2: c < 0 and
A3: delta (a,b,c) = 0 ; :: thesis: a = 0
A4: (b ^2) - ((4 * a) * c) = 0 by A3, QUIN_1:def 1;
0 <= b ^2

proof

per cases ( b = 0 or 0 <> b ) ;

suppose b = 0 ; :: thesis: 0 <= b ^2

hence 0 <= b ^2 ; :: thesis: verum

end;

suppose 0 <> b ; :: thesis: 0 <= b ^2

hence 0 <= b ^2 by SQUARE_1:12; :: thesis: verum

end;

end;

end;

hence a = 0 by A1, A2, A4; :: thesis: verum