now :: thesis:

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:
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:

end;

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

A5: now :: thesis:

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

now :: thesis:

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

end;

hence u in P ; :: thesis:

end;

now :: thesis:

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

end;

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

end;

now :: thesis:

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:
assume f in I ; :: thesis:
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:

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: