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)

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)

hence
PolyRedRel (P,T) c= PolyRedRel (Q,T)
; :: thesis: verumu 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 A4, POLYNOM1:def 11;

0_ (n,L) = 0. (Polynom-Ring (n,L)) by POLYNOM1:def 11;

then not p in {(0_ (n,L))} by A3, XBOOLE_0:def 5;

then p <> 0_ (n,L) by TARSKI:def 1;

then reconsider p = p as non-zero Polynomial of n,L by A3, POLYNOM1:def 11, POLYNOM7:def 1;

p reduces_to q,P,T by A2, A5, POLYRED:def 13;

then p reduces_to q,Q,T by A1, Th3;

hence u in PolyRedRel (Q,T) by A5, POLYRED:def 13; :: thesis: verum

end;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 A4, POLYNOM1:def 11;

0_ (n,L) = 0. (Polynom-Ring (n,L)) by POLYNOM1:def 11;

then not p in {(0_ (n,L))} by A3, XBOOLE_0:def 5;

then p <> 0_ (n,L) by TARSKI:def 1;

then reconsider p = p as non-zero Polynomial of n,L by A3, POLYNOM1:def 11, POLYNOM7:def 1;

p reduces_to q,P,T by A2, A5, POLYRED:def 13;

then p reduces_to q,Q,T by A1, Th3;

hence u in PolyRedRel (Q,T) by A5, POLYRED:def 13; :: thesis: verum