let n be Ordinal; :: thesis: for T being connected admissible TermOrder of n
for L being non empty non degenerated right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr
for f, p, g being Polynomial of n,L st f reduces_to g,p,T holds
for b being bag of n st b in Support g holds
b <= HT f,T,T
let T be connected admissible TermOrder of n; :: thesis: for L being non empty non degenerated right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr
for f, p, g being Polynomial of n,L st f reduces_to g,p,T holds
for b being bag of n st b in Support g holds
b <= HT f,T,T
let L be non empty non degenerated right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr ; :: thesis: for f, p, g being Polynomial of n,L st f reduces_to g,p,T holds
for b being bag of n st b in Support g holds
b <= HT f,T,T
let f, p, g be Polynomial of n,L; :: thesis: ( f reduces_to g,p,T implies for b being bag of n st b in Support g holds
b <= HT f,T,T )
A1: T is_connected_in field T by RELAT_2:def 14;
assume f reduces_to g,p,T ; :: thesis: for b being bag of n st b in Support g holds
b <= HT f,T,T
then consider b being bag of n such that
A2: f reduces_to g,p,b,T by Def6;
b in Support f by A2, Def5;
then A3: b <= HT f,T,T by TERMORD:def 6;

now

let u be bag of n; :: thesis: ( u in Support g implies u <= HT f,T,T )
assume A4: u in Support g ; :: thesis: u <= HT f,T,T

now

per cases ( u = b or u <> b ) ;

case u = b ; :: thesis: contradiction

hence contradiction by A2, A4, Lm17; :: thesis: verum

end;

case A5: u <> b ; :: thesis: u <= HT f,T,T

b <= b,T by TERMORD:6;
then [b,b] in T by TERMORD:def 2;
then A6: b in field T by RELAT_1:30;
u <= u,T by TERMORD:6;
then [u,u] in T by TERMORD:def 2;
then u in field T by RELAT_1:30;
then A7: ( [u,b] in T or [b,u] in T ) by A1, A5, A6, RELAT_2:def 6;

now

per cases ( u <= b,T or b <= u,T ) by A7, TERMORD:def 2;

case u <= b,T ; :: thesis: u <= HT f,T,T

hence u <= HT f,T,T by A3, TERMORD:8; :: thesis: verum

end;

case b <= u,T ; :: thesis: u <= HT f,T,T

then b < u,T by A5, TERMORD:def 3;
then ( u in Support f iff u in Support g ) by A2, Th40;
hence u <= HT f,T,T by A4, TERMORD:def 6; :: thesis: verum

end;

end;

end;

hence u <= HT f,T,T ; :: thesis: verum

end;

end;

end;

hence u <= HT f,T,T ; :: thesis: verum

end;

hence for b being bag of n st b in Support g holds
b <= HT f,T,T ; :: thesis: verum