let IT1, IT2 be strict RelStr ; :: thesis: ( the carrier of IT1 = Bags n & ( for x, y being bag of n holds
( [x,y] in the InternalRel of IT1 iff x divides y ) ) & the carrier of IT2 = Bags n & ( for x, y being bag of n holds
( [x,y] in the InternalRel of IT2 iff x divides y ) ) implies IT1 = IT2 )
assume that
A4: the carrier of IT1 = Bags n and
A5: for x, y being bag of n holds
( [x,y] in the InternalRel of IT1 iff x divides y ) and
A6: the carrier of IT2 = Bags n and
A7: for x, y being bag of n holds
( [x,y] in the InternalRel of IT2 iff x divides y ) ; :: thesis: IT1 = IT2

now :: thesis: for a, b being object holds
( ( [a,b] in the InternalRel of IT1 implies [a,b] in the InternalRel of IT2 ) & ( [a,b] in the InternalRel of IT2 implies [a,b] in the InternalRel of IT1 ) )

let a, b be object ; :: thesis: ( ( [a,b] in the InternalRel of IT1 implies [a,b] in the InternalRel of IT2 ) & ( [a,b] in the InternalRel of IT2 implies [a,b] in the InternalRel of IT1 ) )
set z = [a,b];

hereby :: thesis: ( [a,b] in the InternalRel of IT2 implies [a,b] in the InternalRel of IT1 )

assume A8: [a,b] in the InternalRel of IT1 ; :: thesis: [a,b] in the InternalRel of IT2
then consider a9, b9 being object such that
A9: [a,b] = [a9,b9] and
A10: a9 in Bags n and
A11: b9 in Bags n by A4, RELSET_1:2;
reconsider a9 = a9, b9 = b9 as bag of n by A10, A11;
a9 divides b9 by A5, A8, A9;
hence [a,b] in the InternalRel of IT2 by A7, A9; :: thesis: verum

end;

assume A12: [a,b] in the InternalRel of IT2 ; :: thesis: [a,b] in the InternalRel of IT1
set z = [a,b];
consider a9, b9 being object such that
A13: [a,b] = [a9,b9] and
A14: a9 in Bags n and
A15: b9 in Bags n by A6, A12, RELSET_1:2;
reconsider a9 = a9, b9 = b9 as bag of n by A14, A15;
a9 divides b9 by A7, A12, A13;
hence [a,b] in the InternalRel of IT1 by A5, A13; :: thesis: verum

end;

hence IT1 = IT2 by A4, A6, RELAT_1:def 2; :: thesis: verum