let n be Ordinal; :: thesis: for T being connected TermOrder of n
for L being non empty addLoopStr
for p, q, r being Polynomial of n,L st p <= q,T & q <= r,T holds
p <= r,T
let T be connected TermOrder of n; :: thesis: for L being non empty addLoopStr
for p, q, r being Polynomial of n,L st p <= q,T & q <= r,T holds
p <= r,T
let L be non empty addLoopStr ; :: thesis: for p, q, r being Polynomial of n,L st p <= q,T & q <= r,T holds
p <= r,T
let p, q, r be Polynomial of n,L; :: thesis: ( p <= q,T & q <= r,T implies p <= r,T )
set O = FinOrd RelStr(# (Bags n),T #);
A1: Support r in Fin the carrier of RelStr(# (Bags n),T #) by Lm11;
assume ( p <= q,T & q <= r,T ) ; :: thesis: p <= r,T
then A2: ( [(Support p),(Support q)] in FinOrd RelStr(# (Bags n),T #) & [(Support q),(Support r)] in FinOrd RelStr(# (Bags n),T #) ) ;
( Support p in Fin the carrier of RelStr(# (Bags n),T #) & Support q in Fin the carrier of RelStr(# (Bags n),T #) ) by Lm11;
then [(Support p),(Support r)] in FinOrd RelStr(# (Bags n),T #) by A2, A1, ORDERS_1:5;
hence p <= r,T ; :: thesis: verum