theorem Th4: :: GROEB_1:4

for n being Ordinal
for T being connected TermOrder of n
for L being non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr
for P, Q being Subset of (Polynom-Ring (n,L)) st P c= Q holds
PolyRedRel (P,T) c= PolyRedRel (Q,T)