now :: thesis: not { i where i is Element of NAT : i < 0 } <> {}

set j = the Element of { i where i is Element of NAT : i < 0 } ;
assume { i where i is Element of NAT : i < 0 } <> {} ; :: thesis: contradiction
then the Element of { i where i is Element of NAT : i < 0 } in { i where i is Element of NAT : i < 0 } ;
then ex i being Element of NAT st
( i = the Element of { i where i is Element of NAT : i < 0 } & i < 0 ) ;
hence contradiction ; :: thesis: verum

end;

then reconsider n = {} as Element of NAT ;
let T be connected admissible TermOrder of {}; :: thesis: 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
let L be non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative 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 that
A1: P c= I and
A2: P <> {(0_ ({},L))} ; :: thesis: P is_Groebner_basis_of I,T
reconsider T = T as connected admissible TermOrder of n ;
reconsider P = P as non empty Subset of (Polynom-Ring (n,L)) ;
reconsider I = I as non empty add-closed left-ideal Subset of (Polynom-Ring (n,L)) ;
A3: ex q being Element of P st q <> 0_ (n,L)

proof

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

A5: now :: thesis: for u being object st u in {(0_ (n,L))} holds
u in P

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

now :: thesis: u in P

assume not u in P ; :: thesis: contradiction
then for v being object holds not v in P by A4, A6;
hence contradiction by XBOOLE_0:def 1; :: thesis: verum

end;

hence u in P ; :: thesis: verum

end;

now :: thesis: for u being object st u in P holds
u in {(0_ (n,L))}

let u be object ; :: 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 A4;
hence u in {(0_ (n,L))} by TARSKI:def 1; :: thesis: verum

end;

hence contradiction by A2, A5, TARSKI:2; :: thesis: verum

end;

now :: thesis: for f being non-zero Polynomial of n,L st f in I holds
f is_reducible_wrt P,T

consider p being Element of P such that
A7: p <> 0_ (n,L) by A3;
reconsider p = p as Polynomial of n,L by POLYNOM1:def 11;
reconsider p = p as non-zero Polynomial of n,L by A7, POLYNOM7:def 1;
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
f <> 0_ (n,L) by POLYNOM7:def 1;
then Support f <> {} by POLYNOM7:1;
then HT (f,T) in Support f by TERMORD:def 6;
then ( HT (p,T) = EmptyBag n & EmptyBag n in Support f ) ;
then f is_reducible_wrt p,T by POLYRED:36;
then consider g being Polynomial of n,L such that
A8: f reduces_to g,p,T by POLYRED:def 8;
f reduces_to g,P,T by A8, 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 b9 being bag of n st
( b9 in HT (P,T) & b9 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