let it1, it2 be non empty strict NetStr over S; ( the carrier of it1 = NAT & the mapping of it1 = (a,b) ,... & ( for i, j being Element of it1
for i9, j9 being Element of NAT st i = i9 & j = j9 holds
( i <= j iff i9 <= j9 ) ) & the carrier of it2 = NAT & the mapping of it2 = (a,b) ,... & ( for i, j being Element of it2
for i9, j9 being Element of NAT st i = i9 & j = j9 holds
( i <= j iff i9 <= j9 ) ) implies it1 = it2 )
assume that
A4:
the carrier of it1 = NAT
and
A5:
the mapping of it1 = (a,b) ,...
and
A6:
for i, j being Element of it1
for i9, j9 being Element of NAT st i = i9 & j = j9 holds
( i <= j iff i9 <= j9 )
and
A7:
the carrier of it2 = NAT
and
A8:
the mapping of it2 = (a,b) ,...
and
A9:
for i, j being Element of it2
for i9, j9 being Element of NAT st i = i9 & j = j9 holds
( i <= j iff i9 <= j9 )
; it1 = it2
the InternalRel of it1 = the InternalRel of it2
proof
let x,
y be
object ;
RELAT_1:def 2 ( ( not [x,y] in the InternalRel of it1 or [x,y] in the InternalRel of it2 ) & ( not [x,y] in the InternalRel of it2 or [x,y] in the InternalRel of it1 ) )
hereby ( not [x,y] in the InternalRel of it2 or [x,y] in the InternalRel of it1 )
assume A10:
[x,y] in the
InternalRel of
it1
;
[x,y] in the InternalRel of it2then reconsider i =
x,
j =
y as
Element of
it1 by ZFMISC_1:87;
reconsider i1 =
i,
i2 =
j as
Element of
NAT by A4;
reconsider i9 =
x,
j9 =
y as
Element of
it2 by A4, A7, A10, ZFMISC_1:87;
i <= j
by A10, ORDERS_2:def 5;
then
i1 <= i2
by A6;
then
i9 <= j9
by A9;
hence
[x,y] in the
InternalRel of
it2
by ORDERS_2:def 5;
verum
end;
assume A11:
[x,y] in the
InternalRel of
it2
;
[x,y] in the InternalRel of it1
then reconsider i =
x,
j =
y as
Element of
it2 by ZFMISC_1:87;
reconsider i9 =
x,
j9 =
y as
Element of
it1 by A4, A7, A11, ZFMISC_1:87;
reconsider i1 =
i,
i2 =
j as
Element of
NAT by A7;
i <= j
by A11, ORDERS_2:def 5;
then
i1 <= i2
by A9;
then
i9 <= j9
by A6;
hence
[x,y] in the
InternalRel of
it1
by ORDERS_2:def 5;
verum
end;
hence
it1 = it2
by A4, A5, A7, A8; verum