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 x = Support p,T;
set y = Support q,T;
set rp = Red p,T;
set rq = Red q,T;
set R = RelStr(# (Bags n),T #);
assume that
A2: HT p,T = HT q,T and
A3: Red p,T <= Red q,T,T ; :: thesis: p <= q,T
[(Support (Red p,T)),(Support (Red q,T))] in FinOrd RelStr(# (Bags n),T #) by A3, Def2;
then A4: [(Support (Red p,T)),(Support (Red q,T))] in union (rng (FinOrd-Approx RelStr(# (Bags n),T #))) by BAGORDER:def 17;

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 A5: p <> 0_ n,L ; :: thesis: p <= q,T

then A6: Support p,T <> {} by POLYNOM7:1;
A7: q is non-zero by A1, POLYNOM7:def 2;
A8: p is non-zero by A5, POLYNOM7:def 2;
A9: Support (Red p,T) = (Support p) \ {(HT p,T)} by TERMORD:36
.= (Support p,T) \ {(PosetMax (Support p,T))} by A8, Th24 ;
A10: Support q,T <> {} by A1, POLYNOM7:1;
A11: Support (Red q,T) = (Support q) \ {(HT q,T)} by TERMORD:36
.= (Support q,T) \ {(PosetMax (Support q,T))} by A7, Th24 ;
PosetMax (Support p,T) = HT q,T by A2, A8, Th24
.= PosetMax (Support q,T) by A7, Th24 ;
then [(Support p,T),(Support q,T)] in union (rng (FinOrd-Approx RelStr(# (Bags n),T #))) by A4, A6, A10, A9, A11, 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