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 1;
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 4;
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 4;
dom (FinOrd-Approx RelStr(# (Bags n),T #)) = NAT by BAGORDER:def 14;
then A4: (FinOrd-Approx RelStr(# (Bags n),T #)) . 0 in rng (FinOrd-Approx RelStr(# (Bags n),T #)) by FUNCT_1:3;
( 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 14;
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 15;
then Red (p,T) <= HM (p,T),T ;
hence Red (p,T) < HM (p,T),T by A2, A3; :: 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 :: thesis: not HT ((Red (p,T)),T) = HT (p,T)

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 4; :: 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;