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 :: thesis: ( p <= q,T & q <= p,T implies Support p = Support q )

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 #) ) ;
( 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:4; :: thesis: verum

end;

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