theorem Th18: :: GROEB_2:18

for n being Ordinal
for T being connected TermOrder of n
for L being non trivial right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr
for P being Subset of (Polynom-Ring (n,L))
for p1, p2 being Polynomial of n,L st p1 in P & p2 in P holds
S-Poly (p1,p2,T) in P -Ideal