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

proof

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

suppose b = 0 ; :: thesis: 0 <= b * b

hence 0 <= b * b ; :: thesis: verum

end;

suppose b <> 0 ; :: thesis: 0 <= b * b

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

end;

end;

end;

hence 0 <= delta (a,b,c) by A1, A2, A3; :: thesis: verum