:: deftheorem defines is_a_common_root_of RATFUNC1:def 3 :
for L being non empty unital doubleLoopStr
for p1, p2 being Polynomial of L
for x being Element of L holds
( x is_a_common_root_of p1,p2 iff ( x is_a_root_of p1 & x is_a_root_of p2 ) );