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 G, I being Subset of (Polynom-Ring (n,L)) st ( for b being bag of n st b in HT (I,T) holds
ex b9 being bag of n st
( b9 in HT (G,T) & b9 divides b ) ) holds
HT (I,T) c= multiples (HT (G,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 G, I being Subset of (Polynom-Ring (n,L)) st ( for b being bag of n st b in HT (I,T) holds
ex b9 being bag of n st
( b9 in HT (G,T) & b9 divides b ) ) holds
HT (I,T) c= multiples (HT (G,T))
let L be non trivial right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr ; :: thesis: for G, I being Subset of (Polynom-Ring (n,L)) st ( for b being bag of n st b in HT (I,T) holds
ex b9 being bag of n st
( b9 in HT (G,T) & b9 divides b ) ) holds
HT (I,T) c= multiples (HT (G,T))
let P, I be Subset of (Polynom-Ring (n,L)); :: thesis: ( ( 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 ) ) implies HT (I,T) c= multiples (HT (P,T)) )
assume A1: 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 ) ; :: thesis: HT (I,T) c= multiples (HT (P,T))

now

let u be set ; :: thesis: ( u in HT (I,T) implies u in multiples (HT (P,T)) )
assume A2: u in HT (I,T) ; :: thesis: u in multiples (HT (P,T))
then reconsider u9 = u as Element of Bags n ;
ex b9 being bag of n st
( b9 in HT (P,T) & b9 divides u9 ) by A1, A2;
hence u in multiples (HT (P,T)) ; :: thesis: verum

end;

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