:: deftheorem defines delta QUIN_1:def 1 :
for a, b, c being Complex holds delta (a,b,c) = (b ^2) - ((4 * a) * c);