let n be Element of NAT ; :: thesis: for T being connected admissible TermOrder of n
for L being non empty non degenerated right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for G being Subset of (Polynom-Ring n,L) st not 0_ n,L in G & ( for g being Polynomial of n,L st g in G holds
g is Monomial of n,L ) holds
G is_Groebner_basis_wrt T
let T be connected admissible TermOrder of n; :: thesis: for L being non empty non degenerated right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for G being Subset of (Polynom-Ring n,L) st not 0_ n,L in G & ( for g being Polynomial of n,L st g in G holds
g is Monomial of n,L ) holds
G is_Groebner_basis_wrt T
let L be non empty non degenerated right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; :: thesis: for G being Subset of (Polynom-Ring n,L) st not 0_ n,L in G & ( for g being Polynomial of n,L st g in G holds
g is Monomial of n,L ) holds
G is_Groebner_basis_wrt T
let G be Subset of (Polynom-Ring n,L); :: thesis: ( not 0_ n,L in G & ( for g being Polynomial of n,L st g in G holds
g is Monomial of n,L ) implies G is_Groebner_basis_wrt T )
assume that
A1: not 0_ n,L in G and
A2: for g being Polynomial of n,L st g in G holds
g is Monomial of n,L ; :: thesis: G is_Groebner_basis_wrt T

now

let g1, g2 be Polynomial of n,L; :: thesis: ( g1 in G & g2 in G implies PolyRedRel G,T reduces S-Poly g1,g2,T, 0_ n,L )
assume ( g1 in G & g2 in G ) ; :: thesis: PolyRedRel G,T reduces S-Poly g1,g2,T, 0_ n,L
then ( g1 is Monomial of n,L & g2 is Monomial of n,L ) by A2;
then S-Poly g1,g2,T = 0_ n,L by Th24;
hence PolyRedRel G,T reduces S-Poly g1,g2,T, 0_ n,L by REWRITE1:13; :: thesis: verum

end;

hence G is_Groebner_basis_wrt T by A1, Th30; :: thesis: verum