let n be Ordinal; :: thesis: for T being TermOrder of n
for b1, b2 being bag of st b1 <= b2,T & b2 <= b1,T holds
b1 = b2
let T be TermOrder of n; :: thesis: for b1, b2 being bag of st b1 <= b2,T & b2 <= b1,T holds
b1 = b2
let b1, b2 be bag of ; :: thesis: ( b1 <= b2,T & b2 <= b1,T implies b1 = b2 )
assume ( b1 <= b2,T & b2 <= b1,T ) ; :: thesis: b1 = b2
then A1: ( [b1,b2] in T & [b2,b1] in T ) by Def2;
field T = Bags n by ORDERS_1:97;
then A2: T is_antisymmetric_in Bags n by RELAT_2:def 12;
( b1 is Element of Bags n & b2 is Element of Bags n ) by POLYNOM1:def 14;
hence b1 = b2 by A1, A2, RELAT_2:def 4; :: thesis: verum