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;
then A4: [(Support (Red (p,T))),(Support (Red (q,T)))] in union (rng (FinOrd-Approx RelStr(# (Bags n),T #))) by BAGORDER:def 15;

now :: thesis: ( ( p = 0_ (n,L) & p <= q,T ) or ( p <> 0_ (n,L) & p <= q,T ) )

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;
A8: p is non-zero by A5;
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:35;
then [(Support (p,T)),(Support (q,T))] in FinOrd RelStr(# (Bags n),T #) by BAGORDER:def 15;
hence p <= q,T ; :: thesis: verum

end;

end;

end;

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