:: deftheorem defines positive HURWITZ2:def 9 :
for p being Polynomial of F_Complex holds
( p is positive iff for x being Element of F_Complex st Re x > 0 holds
Re (eval (p,x)) > 0 );