:: deftheorem defines Common_Roots RATFUNC1:def 5 :
for L being non empty unital doubleLoopStr
for p, q being Polynomial of L holds Common_Roots (p,q) = { x where x is Element of L : x is_a_common_root_of p,q } ;