let n be Ordinal; :: thesis: for T being connected TermOrder of n
for L being non empty addLoopStr
for p being Polynomial of n,L holds p <= p,T
let T be connected TermOrder of n; :: thesis: for L being non empty addLoopStr
for p being Polynomial of n,L holds p <= p,T
let L be non empty addLoopStr ; :: thesis: for p being Polynomial of n,L holds p <= p,T
let p be Polynomial of n,L; :: thesis: p <= p,T
set O = FinOrd RelStr(# (Bags n),T #);
[(Support p),(Support p)] in FinOrd RelStr(# (Bags n),T #) by Lm11, ORDERS_1:3;
hence p <= p,T by Def2; :: thesis: verum