:: deftheorem defines positive HURWITZ2:def 14 :
for Z being rational_function of F_Complex holds
( Z is positive iff for x being Element of F_Complex st Re x > 0 & eval ((Z `2),x) <> 0 holds
Re (eval (Z,x)) > 0 );