let B1, B2 be Order of (Bags n); :: thesis: ( ( for p, q being bag of n holds
( [p,q] in B1 iff p <=' q ) ) & ( for p, q being bag of n holds
( [p,q] in B2 iff p <=' q ) ) implies B1 = B2 )
assume that
A17: for p, q being bag of n holds
( [p,q] in B1 iff p <=' q ) and
A18: for p, q being bag of n holds
( [p,q] in B2 iff p <=' q ) ; :: thesis: B1 = B2
let a, b be object ; :: according to RELAT_1:def 2 :: thesis: ( ( not [a,b] in B1 or [a,b] in B2 ) & ( not [a,b] in B2 or [a,b] in B1 ) )

hereby :: thesis: ( not [a,b] in B2 or [a,b] in B1 )

assume A19: [a,b] in B1 ; :: thesis: [a,b] in B2
then consider b1, b2 being object such that
A20: [a,b] = [b1,b2] and
A21: ( b1 in Bags n & b2 in Bags n ) by RELSET_1:2;
reconsider b1 = b1, b2 = b2 as bag of n by A21;
b1 <=' b2 by A17, A19, A20;
hence [a,b] in B2 by A18, A20; :: thesis: verum

end;

assume A22: [a,b] in B2 ; :: thesis: [a,b] in B1
then consider b1, b2 being object such that
A23: [a,b] = [b1,b2] and
A24: ( b1 in Bags n & b2 in Bags n ) by RELSET_1:2;
reconsider b1 = b1, b2 = b2 as bag of n by A24;
b1 <=' b2 by A18, A22, A23;
hence [a,b] in B1 by A17, A23; :: thesis: verum