let B1, B2 be Order of (Bags n); :: thesis: ( ( for b1, b2 being bag of n holds
( [b1,b2] in B1 iff b1 divides b2 ) ) & ( for b1, b2 being bag of n holds
( [b1,b2] in B2 iff b1 divides b2 ) ) implies B1 = B2 )
assume that
A19: for p, q being bag of n holds
( [p,q] in B1 iff p divides q ) and
A20: for p, q being bag of n holds
( [p,q] in B2 iff p divides 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 A21: [a,b] in B1 ; :: thesis: [a,b] in B2
then consider b1, b2 being object such that
A22: [a,b] = [b1,b2] and
A23: ( b1 in Bags n & b2 in Bags n ) by RELSET_1:2;
reconsider b1 = b1, b2 = b2 as bag of n by A23;
b1 divides b2 by A19, A21, A22;
hence [a,b] in B2 by A20, A22; :: thesis: verum

end;

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