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 < p,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 < p,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 < p,T
let p be non-zero Polynomial of n,L; :: thesis: Red p,T < p,T
(Red p,T) . (HT p,T) = 0. L by TERMORD:39;
then A1: not HT p,T in Support (Red p,T) by POLYNOM1:def 9;
p <> 0_ n,L by POLYNOM7:def 2;
then Support p <> {} by POLYNOM7:1;
then A2: HT p,T in Support p by TERMORD:def 6;
Red p,T < HM p,T,T by Th33;
then A3: Red p,T <= HM p,T,T by Def3;
HM p,T <= p,T by Th34;
then Red p,T <= p,T by A3, Th27;
hence Red p,T < p,T by A2, A1, Def3; :: thesis: verum