let n be Ordinal; :: thesis: for T being connected TermOrder of n
for L being non trivial right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr
for P being Subset of (Polynom-Ring n,L) st ( for f being non-zero Polynomial of n,L st f in P -Ideal holds
f is_top_reducible_wrt P,T ) holds
for b being bag of st b in HT (P -Ideal ),T holds
ex b' being bag of st
( b' in HT P,T & b' divides b )
let T be connected TermOrder of n; :: thesis: for L being non trivial right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr
for P being Subset of (Polynom-Ring n,L) st ( for f being non-zero Polynomial of n,L st f in P -Ideal holds
f is_top_reducible_wrt P,T ) holds
for b being bag of st b in HT (P -Ideal ),T holds
ex b' being bag of st
( b' in HT P,T & b' divides b )
let L be non trivial right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr ; :: thesis: for P being Subset of (Polynom-Ring n,L) st ( for f being non-zero Polynomial of n,L st f in P -Ideal holds
f is_top_reducible_wrt P,T ) holds
for b being bag of st b in HT (P -Ideal ),T holds
ex b' being bag of st
( b' in HT P,T & b' divides b )
let P be Subset of (Polynom-Ring n,L); :: thesis: ( ( for f being non-zero Polynomial of n,L st f in P -Ideal holds
f is_top_reducible_wrt P,T ) implies for b being bag of st b in HT (P -Ideal ),T holds
ex b' being bag of st
( b' in HT P,T & b' divides b ) )
assume A1: for f being non-zero Polynomial of n,L st f in P -Ideal holds
f is_top_reducible_wrt P,T ; :: thesis: for b being bag of st b in HT (P -Ideal ),T holds
ex b' being bag of st
( b' in HT P,T & b' divides b )

now

let b be bag of ; :: thesis: ( b in HT (P -Ideal ),T implies ex b' being bag of st
( b' in HT P,T & b' divides b ) )
assume b in HT (P -Ideal ),T ; :: thesis: ex b' being bag of st
( b' in HT P,T & b' divides b )
then consider p being Polynomial of n,L such that
A2: ( b = HT p,T & p in P -Ideal & p <> 0_ n,L ) ;
reconsider p = p as non-zero Polynomial of n,L by A2, POLYNOM7:def 2;
p is_top_reducible_wrt P,T by A1, A2;
then consider u being Polynomial of n,L such that
A3: ( u in P & p is_top_reducible_wrt u,T ) by POLYRED:def 12;
consider q being Polynomial of n,L such that
A4: p top_reduces_to q,u,T by A3, POLYRED:def 11;
A5: p reduces_to q,u, HT p,T,T by A4, POLYRED:def 10;
then consider s being bag of such that
A6: ( s + (HT u,T) = HT p,T & q = p - (((p . (HT p,T)) / (HC u,T)) * (s *' u)) ) by POLYRED:def 5;
u <> 0_ n,L by A5, POLYRED:def 5;
then HT u,T in { (HT r,T) where r is Polynomial of n,L : ( r in P & r <> 0_ n,L ) } by A3;
hence ex b' being bag of st
( b' in HT P,T & b' divides b ) by A2, A6, POLYNOM1:54; :: thesis: verum

end;

hence for b being bag of st b in HT (P -Ideal ),T holds
ex b' being bag of st
( b' in HT P,T & b' divides b ) ; :: thesis: verum