:: deftheorem defines with_roots POLYNOM5:def 8 :
for L being non empty unital doubleLoopStr
for p being Polynomial of L holds
( p is with_roots iff ex x being Element of L st x is_a_root_of p );