let n be Ordinal; :: thesis: 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)

let T be connected TermOrder of n; :: thesis: 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)

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

let P, Q be Subset of (Polynom-Ring (n,L)); :: thesis: ( P c= Q implies PolyRedRel (P,T) c= PolyRedRel (Q,T) )
assume A1: P c= Q ; :: thesis: PolyRedRel (P,T) c= PolyRedRel (Q,T)
now :: thesis: for u being object st u in PolyRedRel (P,T) holds
u in PolyRedRel (Q,T)
let u be object ; :: thesis: ( u in PolyRedRel (P,T) implies u in PolyRedRel (Q,T) )
assume A2: u in PolyRedRel (P,T) ; :: thesis: u in PolyRedRel (Q,T)
then consider p, q being object such that
A3: p in NonZero (Polynom-Ring (n,L)) and
A4: q in the carrier of (Polynom-Ring (n,L)) and
A5: u = [p,q] by ZFMISC_1:def 2;
reconsider q = q as Polynomial of n,L by ;
0_ (n,L) = 0. (Polynom-Ring (n,L)) by POLYNOM1:def 11;
then not p in {(0_ (n,L))} by ;
then p <> 0_ (n,L) by TARSKI:def 1;
then reconsider p = p as non-zero Polynomial of n,L by ;
p reduces_to q,P,T by ;
then p reduces_to q,Q,T by ;
hence u in PolyRedRel (Q,T) by ; :: thesis: verum
end;
hence PolyRedRel (P,T) c= PolyRedRel (Q,T) ; :: thesis: verum