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 & q <= p,T ) iff Support p = Support q )
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 & q <= p,T ) iff Support p = Support q )
let L be non empty addLoopStr ; :: thesis: for p, q being Polynomial of n,L holds
( ( p <= q,T & q <= p,T ) iff Support p = Support q )
let p, q be Polynomial of n,L; :: thesis: ( ( p <= q,T & q <= p,T ) iff Support p = Support q )
set O = FinOrd RelStr(# (Bags n),T #);

A1: now

assume ( p <= q,T & q <= p,T ) ; :: thesis: Support p = Support q
then A2: ( [(Support p),(Support q)] in FinOrd RelStr(# (Bags n),T #) & [(Support q),(Support p)] in FinOrd RelStr(# (Bags n),T #) ) by Def2;
( Support p in Fin the carrier of RelStr(# (Bags n),T #) & Support q in Fin the carrier of RelStr(# (Bags n),T #) ) by Lm11;
hence Support p = Support q by A2, ORDERS_1:13; :: thesis: verum

end;

now

assume Support p = Support q ; :: thesis: ( p <= q,T & q <= p,T )
then ( [(Support p),(Support q)] in FinOrd RelStr(# (Bags n),T #) & [(Support q),(Support p)] in FinOrd RelStr(# (Bags n),T #) ) by Lm11, ORDERS_1:12;
hence ( p <= q,T & q <= p,T ) by Def2; :: thesis: verum

end;

hence ( ( p <= q,T & q <= p,T ) iff Support p = Support q ) by A1; :: thesis: verum