theorem :: GROEB_1:32

for T being connected admissible TermOrder of {}
for L being non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr
for I being non empty add-closed left-ideal Subset of (Polynom-Ring ({},L))
for P being non empty Subset of (Polynom-Ring ({},L)) st P c= I & P <> {(0_ ({},L))} holds
P is_Groebner_basis_of I,T