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 ) )

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

( [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 A24:
[a,b] in B2
; :: thesis: [a,b] in B1assume 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;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

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