for R being non trivial right_complementable Abelian add-associative right_zeroed well-unital distributive associative commutative doubleLoopStr
for X being infinite Ordinal holds not Polynom-Ring (X,R) is Noetherian