theorem :: GROEB_1:23

for n being Element of NAT
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 being Polynomial of n,L
for P being non empty Subset of (Polynom-Ring (n,L)) st P is_Groebner_basis_wrt T holds
( f in P -Ideal iff PolyRedRel (P,T) reduces f, 0_ (n,L) ) by Th15, POLYRED:60;