let B1, B2 be Order of (Bags n); :: thesis: ( ( for p, q being bag of holds
( [p,q] in B1 iff p <=' q ) ) & ( for p, q being bag of holds
( [p,q] in B2 iff p <=' q ) ) implies B1 = B2 )
assume that
A13: for p, q being bag of holds
( [p,q] in B1 iff p <=' q ) and
A14: for p, q being bag of holds
( [p,q] in B2 iff p <=' q ) ; :: thesis: B1 = B2
let a, b be set ; :: 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 A15: [a,b] in B1 ; :: thesis: [a,b] in B2
then consider b1, b2 being set such that
A16: ( [a,b] = [b1,b2] & b1 in Bags n & b2 in Bags n ) by RELSET_1:6;
reconsider b1 = b1, b2 = b2 as bag of by A16, Def14;
b1 <=' b2 by A13, A15, A16;
hence [a,b] in B2 by A14, A16; :: thesis: verum

end;

assume A17: [a,b] in B2 ; :: thesis: [a,b] in B1
then consider b1, b2 being set such that
A18: ( [a,b] = [b1,b2] & b1 in Bags n & b2 in Bags n ) by RELSET_1:6;
reconsider b1 = b1, b2 = b2 as bag of by A18, Def14;
b1 <=' b2 by A14, A17, A18;
hence [a,b] in B1 by A13, A18; :: thesis: verum