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

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

hence
it1 = it2
by A4, A5, A7, A8; :: thesis: verum
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 ) )

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; :: thesis: verum

end;hereby :: thesis: ( not [x,y] in the InternalRel of it2 or [x,y] in the InternalRel of it1 )

assume A11:
[x,y] in the InternalRel of it2
; :: thesis: [x,y] in the InternalRel of it1assume 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 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; :: thesis: verum

end;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 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; :: thesis: verum

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; :: thesis: verum