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 {p} is_Groebner_basis_of {p} -Ideal ,T