let n be Element of NAT ; :: thesis: 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
let T be connected admissible TermOrder of n; :: thesis: 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
let L be non trivial right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr ; :: thesis: for p being Polynomial of n,L holds {p} is_Groebner_basis_of {p} -Ideal ,T
let p be Polynomial of n,L; :: thesis: {p} is_Groebner_basis_of {p} -Ideal ,T

per cases ( p = 0_ (n,L) or p <> 0_ (n,L) ) ;

suppose A1: p = 0_ (n,L) ; :: thesis: {p} is_Groebner_basis_of {p} -Ideal ,T

0_ (n,L) = 0. (Polynom-Ring (n,L)) by POLYNOM1:def 11;
then {p} -Ideal = {(0_ (n,L))} by A1, IDEAL_1:44;
hence {p} is_Groebner_basis_of {p} -Ideal ,T by A1, Th30; :: thesis: verum

end;

suppose p <> 0_ (n,L) ; :: thesis: {p} is_Groebner_basis_of {p} -Ideal ,T

then reconsider p = p as non-zero Polynomial of n,L by POLYNOM7:def 1;
PolyRedRel ({p},T) is locally-confluent by Th10;
hence {p} is_Groebner_basis_of {p} -Ideal ,T ; :: thesis: verum

end;

end;