let it1, it2 be non empty strict NetStr of L; :: thesis: ( 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
; :: thesis: it1 = it2
set S = { [a,f] where a is Element of L, f is Element of F : a in f } ;
A12:
the InternalRel of it1 = the InternalRel of it2
proof
for
x,
y being
set holds
(
[x,y] in the
InternalRel of
it1 iff
[x,y] in the
InternalRel of
it2 )
proof
let x,
y be
set ;
:: thesis: ( [x,y] in the InternalRel of it1 iff [x,y] in the InternalRel of it2 )
assume A14:
[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:106;
reconsider i' =
x,
j' =
y as
Element of
it1 by A6, A9, A14, ZFMISC_1:106;
i <= j
by A14, ORDERS_2:def 9;
then
j' `2 c= i' `2
by A10;
then
i' <= j'
by A7;
hence
[x,y] in the
InternalRel of
it1
by ORDERS_2:def 9;
:: thesis: verum
end;
hence
the
InternalRel of
it1 = the
InternalRel of
it2
by RELAT_1:def 2;
:: thesis: verum
end;
the mapping of it1 = the mapping of it2
hence
it1 = it2
by A6, A9, A12; :: thesis: verum