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 f, g being Polynomial of n,L
for P, Q being Subset of (Polynom-Ring (n,L)) st P c= Q & f reduces_to g,P,T holds
f reduces_to g,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 f, g being Polynomial of n,L
for P, Q being Subset of (Polynom-Ring (n,L)) st P c= Q & f reduces_to g,P,T holds
f reduces_to g,Q,T
let L be non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr ; :: thesis: for f, g being Polynomial of n,L
for P, Q being Subset of (Polynom-Ring (n,L)) st P c= Q & f reduces_to g,P,T holds
f reduces_to g,Q,T
let f, g be Polynomial of n,L; :: thesis: for P, Q being Subset of (Polynom-Ring (n,L)) st P c= Q & f reduces_to g,P,T holds
f reduces_to g,Q,T
let P, Q be Subset of (Polynom-Ring (n,L)); :: thesis: ( P c= Q & f reduces_to g,P,T implies f reduces_to g,Q,T )
assume A1: P c= Q ; :: thesis: ( not f reduces_to g,P,T or f reduces_to g,Q,T )
assume f reduces_to g,P,T ; :: thesis: f reduces_to g,Q,T
then ex p being Polynomial of n,L st
( p in P & f reduces_to g,p,T ) by POLYRED:def 7;
hence f reduces_to g,Q,T by A1, POLYRED:def 7; :: thesis: verum