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 ;
reconsider a9 = a9, b9 = b9 as bag of n by ;
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 ;
reconsider a9 = a9, b9 = b9 as bag of n by ;
a9 divides b9 by A7, A12, A13;
hence [a,b] in the InternalRel of IT1 by ; :: thesis: verum
end;
hence IT1 = IT2 by ; :: thesis: verum