let n be Ordinal; 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 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; for L being non trivial right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed 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 associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr ; 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)); ( P c= Q implies PolyRedRel (P,T) c= PolyRedRel (Q,T) )
assume A1:
P c= Q
; PolyRedRel (P,T) c= PolyRedRel (Q,T)
now let u be
set ;
( u in PolyRedRel (P,T) implies u in PolyRedRel (Q,T) )assume A2:
u in PolyRedRel (
P,
T)
;
u in PolyRedRel (Q,T)then consider p,
q being
set 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 10;
0_ (
n,
L)
= 0. (Polynom-Ring (n,L))
by POLYNOM1:def 10;
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 10, 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;
verum end;
hence
PolyRedRel (P,T) c= PolyRedRel (Q,T)
by TARSKI:def 3; verum