set S = { [a,f] where a is Element of L, f is Element of F : a in f } ;
let it1, it2 be non empty strict NetStr over L; ( the carrier of it1 = { [a,f] where a is Element of L, f is Element of F : a in f } & ( for i, j being Element of it1 holds
( i <= j iff j `2 c= i `2 ) ) & ( for i being Element of it1 holds it1 . i = i `1 ) & the carrier of it2 = { [a,f] where a is Element of L, f is Element of F : a in f } & ( for i, j being Element of it2 holds
( i <= j iff j `2 c= i `2 ) ) & ( for i being Element of it2 holds it2 . i = i `1 ) implies it1 = it2 )
assume that
A6:
the carrier of it1 = { [a,f] where a is Element of L, f is Element of F : a in f }
and
A7:
for i, j being Element of it1 holds
( i <= j iff j `2 c= i `2 )
and
A8:
for i being Element of it1 holds it1 . i = i `1
and
A9:
the carrier of it2 = { [a,f] where a is Element of L, f is Element of F : a in f }
and
A10:
for i, j being Element of it2 holds
( i <= j iff j `2 c= i `2 )
and
A11:
for i being Element of it2 holds it2 . i = i `1
; it1 = it2
A12:
for x, y being object holds
( [x,y] in the InternalRel of it1 iff [x,y] in the InternalRel of it2 )
proof
let x,
y be
object ;
( [x,y] in the InternalRel of it1 iff [x,y] in the InternalRel of it2 )
assume A14:
[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 A6, A9, A14, ZFMISC_1:87;
i <= j
by A14, ORDERS_2:def 5;
then
j9 `2 c= i9 `2
by A10;
then
i9 <= j9
by A7;
hence
[x,y] in the
InternalRel of
it1
by ORDERS_2:def 5;
verum
end;
the mapping of it1 = the mapping of it2
hence
it1 = it2
by A6, A9, A12, RELAT_1:def 2; verum