:: deftheorem defines Tri POLYEQ_1:def 5 :
for a, x, x1, x2, x3 being Complex holds Tri (a,x1,x2,x3,x) = a * (((x - x1) * (x - x2)) * (x - x3));