let n be Ordinal; :: thesis: for T being connected admissible TermOrder of n
for L being non trivial right_complementable add-associative right_zeroed addLoopStr
for p, q being Polynomial of n,L st q <> 0_ n,L & HT p,T = HT q,T & Red p,T <= Red q,T,T holds
p <= q,T
let T be connected admissible TermOrder of n; :: thesis: for L being non trivial right_complementable add-associative right_zeroed addLoopStr
for p, q being Polynomial of n,L st q <> 0_ n,L & HT p,T = HT q,T & Red p,T <= Red q,T,T holds
p <= q,T
let L be non trivial right_complementable add-associative right_zeroed addLoopStr ; :: thesis: for p, q being Polynomial of n,L st q <> 0_ n,L & HT p,T = HT q,T & Red p,T <= Red q,T,T holds
p <= q,T
let p, q be Polynomial of n,L; :: thesis: ( q <> 0_ n,L & HT p,T = HT q,T & Red p,T <= Red q,T,T implies p <= q,T )
assume A1: q <> 0_ n,L ; :: thesis: ( not HT p,T = HT q,T or not Red p,T <= Red q,T,T or p <= q,T )
set R = RelStr(# (Bags n),T #);
assume A2: ( HT p,T = HT q,T & Red p,T <= Red q,T,T ) ; :: thesis: p <= q,T
then [(Support (Red p,T)),(Support (Red q,T))] in FinOrd RelStr(# (Bags n),T #) by Def2;
then A3: [(Support (Red p,T)),(Support (Red q,T))] in union (rng (FinOrd-Approx RelStr(# (Bags n),T #))) by BAGORDER:def 17;
set rp = Red p,T;
set rq = Red q,T;
set x = Support p,T;
set y = Support q,T;

now

per cases ( p = 0_ n,L or p <> 0_ n,L ) ;

case p = 0_ n,L ; :: thesis: p <= q,T

hence p <= q,T by Lm12; :: thesis: verum

end;

case A4: p <> 0_ n,L ; :: thesis: p <= q,T

then A5: p is non-zero by POLYNOM7:def 2;
A6: q is non-zero by A1, POLYNOM7:def 2;
A7: ( Support p,T <> {} & Support q,T <> {} ) by A1, A4, POLYNOM7:1;
A8: PosetMax (Support p,T) = HT q,T by A2, A5, Th24
.= PosetMax (Support q,T) by A6, Th24 ;
A9: Support (Red p,T) = (Support p) \ {(HT p,T)} by TERMORD:36
.= (Support p,T) \ {(PosetMax (Support p,T))} by A5, Th24 ;
Support (Red q,T) = (Support q) \ {(HT q,T)} by TERMORD:36
.= (Support q,T) \ {(PosetMax (Support q,T))} by A6, Th24 ;
then [(Support p,T),(Support q,T)] in union (rng (FinOrd-Approx RelStr(# (Bags n),T #))) by A3, A7, A8, A9, BAGORDER:36;
then [(Support p,T),(Support q,T)] in FinOrd RelStr(# (Bags n),T #) by BAGORDER:def 17;
hence p <= q,T by Def2; :: thesis: verum

end;

end;

end;

hence p <= q,T ; :: thesis: verum