:: deftheorem defines is_Groebner_basis_wrt GROEB_1:def 3 :
for n being Ordinal
for T being connected TermOrder of n
for L being non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr
for G being Subset of (Polynom-Ring (n,L)) holds
( G is_Groebner_basis_wrt T iff PolyRedRel (G,T) is locally-confluent );