:: deftheorem polymem1 defines -polynomial-membered RING_4:def 2 :
for L being non empty ZeroStr
for X being 1-sorted holds
( X is L -polynomial-membered iff the carrier of X is L -polynomial-membered );