let R1, R2 be non empty reflexive RelStr ; :: thesis: for X being non empty set st RelStr(# the carrier of R1,the InternalRel of R1 #) = RelStr(# the carrier of R2,the InternalRel of R2 #) holds
for N1 being net of R1
for N2 being net of R2 st N1 = N2 holds
for J1 being net_set of the carrier of N1,R1 holds J1 is net_set of the carrier of N2,R2
let X be non empty set ; :: thesis: ( RelStr(# the carrier of R1,the InternalRel of R1 #) = RelStr(# the carrier of R2,the InternalRel of R2 #) implies for N1 being net of R1
for N2 being net of R2 st N1 = N2 holds
for J1 being net_set of the carrier of N1,R1 holds J1 is net_set of the carrier of N2,R2 )
assume A1: RelStr(# the carrier of R1,the InternalRel of R1 #) = RelStr(# the carrier of R2,the InternalRel of R2 #) ; :: thesis: for N1 being net of R1
for N2 being net of R2 st N1 = N2 holds
for J1 being net_set of the carrier of N1,R1 holds J1 is net_set of the carrier of N2,R2
let N1 be net of R1; :: thesis: for N2 being net of R2 st N1 = N2 holds
for J1 being net_set of the carrier of N1,R1 holds J1 is net_set of the carrier of N2,R2
let N2 be net of R2; :: thesis: ( N1 = N2 implies for J1 being net_set of the carrier of N1,R1 holds J1 is net_set of the carrier of N2,R2 )
assume A2: N1 = N2 ; :: thesis: for J1 being net_set of the carrier of N1,R1 holds J1 is net_set of the carrier of N2,R2
let J1 be net_set of the carrier of N1,R1; :: thesis: J1 is net_set of the carrier of N2,R2
reconsider J2 = J1 as ManySortedSet of by A2;
for i being set st i in rng J2 holds
i is net of R2

proof

let i be set ; :: thesis: ( i in rng J2 implies i is net of R2 )
assume i in rng J2 ; :: thesis: i is net of R2
then reconsider N = i as net of R1 by YELLOW_6:def 15;
N is NetStr of R2 by A1;
hence i is net of R2 ; :: thesis: verum

end;

hence J1 is net_set of the carrier of N2,R2 by YELLOW_6:def 15; :: thesis: verum