theorem Th27: :: GROEB_1:27

for n being Ordinal
for T being connected TermOrder of n
for L being non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr
for G, I being Subset of (Polynom-Ring (n,L)) st ( for f being non-zero Polynomial of n,L st f in I holds
f is_top_reducible_wrt G,T ) holds
for b being bag of n st b in HT (I,T) holds
ex b9 being bag of n st
( b9 in HT (G,T) & b9 divides b )