for n being Ordinal
for T being connected admissible TermOrder of n
for L being non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr
for f, p, g being Polynomial of n,L st f reduces_to g,p,T holds
ex m being Monomial of n,L st
( g = f - (m *' p) & not HT ((m *' p),T) in Support g & HT ((m *' p),T) <= HT (f,T),T )