:: deftheorem polymem defines -polynomial-membered RING_4:def 1 :
for L being non empty ZeroStr
for X being set holds
( X is L -polynomial-membered iff for p being object st p in X holds
p is Polynomial of L );