:: deftheorem defines have_a_common_root RATFUNC1:def 4 :
for L being non empty unital doubleLoopStr
for p1, p2 being Polynomial of L holds
( p1,p2 have_a_common_root iff ex x being Element of L st x is_a_common_root_of p1,p2 );