:: deftheorem Def10 defines Roots POLYNOM5:def 10 :
for L being non empty unital doubleLoopStr
for p being Polynomial of L
for b₃ being Subset of L holds
( b₃ = Roots p iff for x being Element of L holds
( x in b₃ iff x is_a_root_of p ) );