theorem Th10: :: GROEB_1:10

for n being Element of NAT
for T being connected admissible 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 Polynomial of n,L holds PolyRedRel ({p},T) is locally-confluent