let n be Ordinal; :: thesis: 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; :: thesis: 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 ; :: 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 let u be
set ;
:: thesis: ( u in PolyRedRel P,T implies u in PolyRedRel Q,T )assume A2:
u in PolyRedRel P,
T
;
:: thesis: u in PolyRedRel Q,Tthen consider p,
q being
set such that A3:
(
p in NonZero (Polynom-Ring n,L) &
q in the
carrier of
(Polynom-Ring n,L) &
u = [p,q] )
by ZFMISC_1:def 2;
reconsider q =
q as
Polynomial of
n,
L by A3, POLYNOM1:def 27;
0_ n,
L = 0. (Polynom-Ring n,L)
by POLYNOM1:def 27;
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 27, POLYNOM7:def 2;
p reduces_to q,
P,
T
by A2, A3, POLYRED:def 13;
then
p reduces_to q,
Q,
T
by A1, Th3;
hence
u in PolyRedRel Q,
T
by A3, POLYRED:def 13;
:: thesis: verum end;
hence
PolyRedRel P,T c= PolyRedRel Q,T
by TARSKI:def 3; :: thesis: verum