let it1, it2 be non empty strict NetStr over S; :: thesis: ( 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 ) ; :: thesis: it1 = it2
the InternalRel of it1 = the InternalRel of it2
proof
let x, y be object ; :: according to RELAT_1:def 2 :: thesis: ( ( 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 :: thesis: ( 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 ; :: thesis: [x,y] in the InternalRel of it2
then 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 ;
i <= j by ;
then i1 <= i2 by A6;
then i9 <= j9 by A9;
hence [x,y] in the InternalRel of it2 by ORDERS_2:def 5; :: thesis: verum
end;
assume A11: [x,y] in the InternalRel of it2 ; :: thesis: [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 ;
reconsider i1 = i, i2 = j as Element of NAT by A7;
i <= j by ;
then i1 <= i2 by A9;
then i9 <= j9 by A6;
hence [x,y] in the InternalRel of it1 by ORDERS_2:def 5; :: thesis: verum
end;
hence it1 = it2 by A4, A5, A7, A8; :: thesis: verum