let it1, it2 be non empty strict NetStr over R; ( 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 )
; 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 A8:
[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 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;
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 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;
verum
end;
hence
it1 = it2
by A2, A3, A5, A6; verum