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 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 ) ) holds
HT (P -Ideal ),T c= multiples (HT P,T)
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 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 ) ) holds
HT (P -Ideal ),T c= multiples (HT P,T)
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 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 ) ) holds
HT (P -Ideal ),T c= multiples (HT P,T)
let P be Subset of (Polynom-Ring n,L); :: 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 ) ) implies HT (P -Ideal ),T c= multiples (HT P,T) )
assume A1: 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: HT (P -Ideal ),T c= multiples (HT P,T)

now

let u be set ; :: thesis: ( u in HT (P -Ideal ),T implies u in multiples (HT P,T) )
assume A2: u in HT (P -Ideal ),T ; :: thesis: u in multiples (HT P,T)
then consider p being Polynomial of n,L such that
A3: ( u = HT p,T & p in P -Ideal & p <> 0_ n,L ) ;
reconsider u' = u as Element of Bags n by A3;
consider b' being bag of such that
A4: ( b' in HT P,T & b' divides u' ) by A1, A2;
thus u in multiples (HT P,T) by A4; :: thesis: verum

end;

hence HT (P -Ideal ),T c= multiples (HT P,T) by TARSKI:def 3; :: thesis: verum