let it1, it2 be non empty strict NetStr over R; :: thesis: ( the carrier of it1 = S & the mapping of it1 = f & ( for i, j being Element of it1 holds
( i <= j iff it1 . i <= it1 . j ) ) & the carrier of it2 = S & the mapping of it2 = f & ( for i, j being Element of it2 holds
( i <= j iff it2 . i <= it2 . j ) ) implies it1 = it2 )
assume that
A2: the carrier of it1 = S and
A3: the mapping of it1 = f and
A4: for i, j being Element of it1 holds
( i <= j iff it1 . i <= it1 . j ) and
A5: the carrier of it2 = S and
A6: the mapping of it2 = f and
A7: for i, j being Element of it2 holds
( i <= j iff it2 . i <= it2 . j ) ; :: 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 A8: [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 i9 = x, j9 = y as Element of it2 by A2, A5, A8, ZFMISC_1:87;
A9: it1 . i = it2 . i9 by A3, A6;
A10: it1 . j = it2 . j9 by A3, A6;
i <= j by A8, ORDERS_2:def 5;
then it2 . i9 <= it2 . j9 by A4, A9, A10;
then i9 <= j9 by A7;
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 A2, A5, A11, ZFMISC_1:87;
A12: it2 . i = it1 . i9 by A3, A6;
A13: it2 . j = it1 . j9 by A3, A6;
i <= j by A11, ORDERS_2:def 5;
then it1 . i9 <= it1 . j9 by A7, A12, A13;
then i9 <= j9 by A4;
hence [x,y] in the InternalRel of it1 by ORDERS_2:def 5; :: thesis: verum

end;

hence it1 = it2 by A2, A3, A5, A6; :: thesis: verum