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

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

hence
IT1 = IT2
by A4, A6, RELAT_1:def 2; :: thesis: verum( ( [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];

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;set z = [a,b];

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

assume A12:
[a,b] in the InternalRel of IT2
; :: thesis: [a,b] in the InternalRel of IT1assume 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;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

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