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 being non-zero Polynomial of n,L holds Red p,T < HM p,T,T
let T be connected admissible TermOrder of n; :: thesis: for L being non trivial right_complementable add-associative right_zeroed addLoopStr
for p being non-zero Polynomial of n,L holds Red p,T < HM p,T,T
let L be non trivial right_complementable add-associative right_zeroed addLoopStr ; :: thesis: for p being non-zero Polynomial of n,L holds Red p,T < HM p,T,T
let p be non-zero Polynomial of n,L; :: thesis: Red p,T < HM p,T,T
set red = Red p,T;
set htp = HT p,T;
set sred = Support (Red p,T);
set sp = Support (HM p,T);
set R = RelStr(# (Bags n),T #);
p <> 0_ n,L by POLYNOM7:def 2;
then A1: Support p <> {} by POLYNOM7:1;

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

suppose Red p,T = 0_ n,L ; :: thesis: Red p,T < HM p,T,T

then A2: Support (Red p,T) = {} by POLYNOM7:1;
HT p,T in Support p by A1, TERMORD:def 6;
then p . (HT p,T) <> 0. L by POLYNOM1:def 9;
then (HM p,T) . (HT p,T) <> 0. L by TERMORD:18;
then A3: HT p,T in Support (HM p,T) by POLYNOM1:def 9;
dom (FinOrd-Approx RelStr(# (Bags n),T #)) = NAT by BAGORDER:def 16;
then A4: (FinOrd-Approx RelStr(# (Bags n),T #)) . 0 in rng (FinOrd-Approx RelStr(# (Bags n),T #)) by FUNCT_1:12;
( Support (Red p,T) is Element of Fin the carrier of RelStr(# (Bags n),T #) & Support (HM p,T) is Element of Fin the carrier of RelStr(# (Bags n),T #) ) by Lm11;
then [(Support (Red p,T)),(Support (HM p,T))] in { [x,y] where x, y is Element of Fin the carrier of RelStr(# (Bags n),T #) : ( x = {} or ( x <> {} & y <> {} & PosetMax x <> PosetMax y & [(PosetMax x),(PosetMax y)] in the InternalRel of RelStr(# (Bags n),T #) ) ) } by A2;
then [(Support (Red p,T)),(Support (HM p,T))] in (FinOrd-Approx RelStr(# (Bags n),T #)) . 0 by BAGORDER:def 16;
then [(Support (Red p,T)),(Support (HM p,T))] in union (rng (FinOrd-Approx RelStr(# (Bags n),T #))) by A4, TARSKI:def 4;
then [(Support (Red p,T)),(Support (HM p,T))] in FinOrd RelStr(# (Bags n),T #) by BAGORDER:def 17;
then Red p,T <= HM p,T,T by Def2;
hence Red p,T < HM p,T,T by A2, A3, Def3; :: thesis: verum

end;

suppose Red p,T <> 0_ n,L ; :: thesis: Red p,T < HM p,T,T

then Support (Red p,T) <> {} by POLYNOM7:1;
then A5: HT (Red p,T),T in Support (Red p,T) by TERMORD:def 6;

A6: now

assume HT (Red p,T),T = HT p,T ; :: thesis: contradiction
then (Red p,T) . (HT (Red p,T),T) = 0. L by TERMORD:39;
hence contradiction by A5, POLYNOM1:def 9; :: thesis: verum

end;

Support (Red p,T) c= Support p by TERMORD:35;
then HT (Red p,T),T <= HT p,T,T by A5, TERMORD:def 6;
then HT (Red p,T),T < HT p,T,T by A6, TERMORD:def 3;
then HT (Red p,T),T < HT (HM p,T),T,T by TERMORD:26;
hence Red p,T < HM p,T,T by Lm15; :: thesis: verum

end;

end;