let T be connected admissible TermOrder of {} ; :: 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 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
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 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
let I be non empty add-closed left-ideal Subset of (Polynom-Ring {} ,L); :: thesis: 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
let P be non empty Subset of (Polynom-Ring {} ,L); :: thesis: ( P c= I & P <> {(0_ {} ,L)} implies P is_Groebner_basis_of I,T )
assume A1: ( P c= I & P <> {(0_ {} ,L)} ) ; :: thesis: P is_Groebner_basis_of I,T

now

assume A2: { i where i is Element of NAT : i < 0 } <> {} ; :: thesis: contradiction
consider j being Element of { i where i is Element of NAT : i < 0 } ;
j in { i where i is Element of NAT : i < 0 } by A2;
then consider i being Element of NAT such that
A3: ( i = j & i < 0 ) ;
thus contradiction by A3, NAT_1:2; :: thesis: verum

end;

then reconsider n = {} as Element of NAT ;
reconsider I = I as non empty add-closed left-ideal Subset of (Polynom-Ring n,L) ;
reconsider P = P as non empty Subset of (Polynom-Ring n,L) ;
reconsider T = T as connected admissible TermOrder of n ;
A4: ex q being Element of P st q <> 0_ n,L

proof

assume A5: for q being Element of P holds not q <> 0_ n,L ; :: thesis: contradiction

A6: now

let u be set ; :: thesis: ( u in P implies u in {(0_ n,L)} )
assume u in P ; :: thesis: u in {(0_ n,L)}
then u = 0_ n,L by A5;
hence u in {(0_ n,L)} by TARSKI:def 1; :: thesis: verum

end;

now

let u be set ; :: thesis: ( u in {(0_ n,L)} implies u in P )
assume u in {(0_ n,L)} ; :: thesis: u in P
then A7: u = 0_ n,L by TARSKI:def 1;

now

assume not u in P ; :: thesis: contradiction
then for v being set holds not v in P by A5, A7;
hence contradiction by XBOOLE_0:def 1; :: thesis: verum

end;

hence u in P ; :: thesis: verum

end;

hence contradiction by A1, A6, TARSKI:2; :: thesis: verum

end;

now

let f be non-zero Polynomial of n,L; :: thesis: ( f in I implies f is_reducible_wrt P,T )
assume f in I ; :: thesis: f is_reducible_wrt P,T
consider p being Element of P such that
A8: p <> 0_ n,L by A4;
reconsider p = p as Polynomial of n,L by POLYNOM1:def 27;
reconsider p = p as non-zero Polynomial of n,L by A8, POLYNOM7:def 2;
A9: HT p,T = EmptyBag n by POLYNOM7:3;
f <> 0_ n,L by POLYNOM7:def 2;
then Support f <> {} by POLYNOM7:1;
then HT f,T in Support f by TERMORD:def 6;
then EmptyBag n in Support f by POLYNOM7:3;
then f is_reducible_wrt p,T by A9, POLYRED:36;
then consider g being Polynomial of n,L such that
A10: f reduces_to g,p,T by POLYRED:def 8;
f reduces_to g,P,T by A10, POLYRED:def 7;
hence f is_reducible_wrt P,T by POLYRED:def 9; :: thesis: verum

end;

then for f being non-zero Polynomial of n,L st f in I holds
f is_top_reducible_wrt P,T by A1, Th26;
then for b being bag of n st b in HT I,T holds
ex b' being bag of n st
( b' in HT P,T & b' divides b ) by Th27;
then HT I,T c= multiples (HT P,T) by Th28;
hence P is_Groebner_basis_of I,T by A1, Th29; :: thesis: verum