let n be Ordinal; :: thesis: for T being connected TermOrder of n
for L being non empty addLoopStr
for p, q being Polynomial of n,L holds
( p <= q,T or q <= p,T )
let T be connected TermOrder of n; :: thesis: for L being non empty addLoopStr
for p, q being Polynomial of n,L holds
( p <= q,T or q <= p,T )
let L be non empty addLoopStr ; :: thesis: for p, q being Polynomial of n,L holds
( p <= q,T or q <= p,T )
let p, q be Polynomial of n,L; :: thesis: ( p <= q,T or q <= p,T )
set R = RelStr(# (Bags n),T #);
set O = RelStr(# (Fin the carrier of RelStr(# (Bags n),T #)),(FinOrd RelStr(# (Bags n),T #)) #);
reconsider sp = Support p, sq = Support q as Element of RelStr(# (Fin the carrier of RelStr(# (Bags n),T #)),(FinOrd RelStr(# (Bags n),T #)) #) by Lm11;
FinPoset RelStr(# (Bags n),T #) is connected ;
then RelStr(# (Fin the carrier of RelStr(# (Bags n),T #)),(FinOrd RelStr(# (Bags n),T #)) #) is connected by BAGORDER:def 16;
then ( sp <= sq or sq <= sp ) by WAYBEL_0:def 29;
then ( [(Support p),(Support q)] in FinOrd RelStr(# (Bags n),T #) or [(Support q),(Support p)] in FinOrd RelStr(# (Bags n),T #) ) by ORDERS_2:def 5;
hence ( p <= q,T or q <= p,T ) ; :: thesis: verum