let R1, R2 be Relation of (Bags I); :: thesis: ( ( for b1, b2 being bag of I holds
( [b1,b2] in R1 iff ( b1 <> b2 & b1 divides b2 ) ) ) & ( for b1, b2 being bag of I holds
( [b1,b2] in R2 iff ( b1 <> b2 & b1 divides b2 ) ) ) implies R1 = R2 )
assume that
A1: for b1, b2 being bag of I holds
( [b1,b2] in R1 iff ( b1 <> b2 & b1 divides b2 ) ) and
A2: for b1, b2 being bag of I holds
( [b1,b2] in R2 iff ( b1 <> b2 & b1 divides b2 ) ) ; :: thesis: R1 = R2
let b1, b2 be Element of Bags I; :: according to RELSET_1:def 2 :: thesis: ( ( not [b1,b2] in R1 or [b1,b2] in R2 ) & ( not [b1,b2] in R2 or [b1,b2] in R1 ) )
( [b1,b2] in R1 iff ( b1 <> b2 & b1 divides b2 ) ) by A1;
hence ( ( not [b1,b2] in R1 or [b1,b2] in R2 ) & ( not [b1,b2] in R2 or [b1,b2] in R1 ) ) by A2; :: thesis: verum