let IT1, IT2 be strict RelStr ; :: thesis: ( the carrier of IT1 = Bags n & ( for x, y being bag of holds
( [x,y] in the InternalRel of IT1 iff x divides y ) ) & the carrier of IT2 = Bags n & ( for x, y being bag of holds
( [x,y] in the InternalRel of IT2 iff x divides y ) ) implies IT1 = IT2 )
assume that
A3:
( the carrier of IT1 = Bags n & ( for x, y being bag of holds
( [x,y] in the InternalRel of IT1 iff x divides y ) ) )
and
A4:
( the carrier of IT2 = Bags n & ( for x, y being bag of holds
( [x,y] in the InternalRel of IT2 iff x divides y ) ) )
; :: thesis: IT1 = IT2
now thus
the
carrier of
IT1 = the
carrier of
IT2
by A3, A4;
:: thesis: the InternalRel of IT1 = the InternalRel of IT2now let a,
b be
set ;
:: 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 A5:
[a,b] in the
InternalRel of
IT1
;
:: thesis: [a,b] in the InternalRel of IT2then consider a',
b' being
set such that A6:
[a,b] = [a',b']
and A7:
(
a' in Bags n &
b' in Bags n )
by A3, RELSET_1:6;
reconsider a' =
a',
b' =
b' as
bag of
by A7, POLYNOM1:def 14;
a' divides b'
by A3, A5, A6;
hence
[a,b] in the
InternalRel of
IT2
by A4, A6;
:: thesis: verum
end; assume A8:
[a,b] in the
InternalRel of
IT2
;
:: thesis: [a,b] in the InternalRel of IT1set z =
[a,b];
consider a',
b' being
set such that A9:
[a,b] = [a',b']
and A10:
(
a' in Bags n &
b' in Bags n )
by A4, A8, RELSET_1:6;
reconsider a' =
a',
b' =
b' as
bag of
by A10, POLYNOM1:def 14;
a' divides b'
by A4, A8, A9;
hence
[a,b] in the
InternalRel of
IT1
by A3, A9;
:: thesis: verum end; hence
the
InternalRel of
IT1 = the
InternalRel of
IT2
by RELAT_1:def 2;
:: thesis: verum end;
hence
IT1 = IT2
; :: thesis: verum