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 the carrier of N2 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 12;
N is NetStr over 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 12; :: thesis: verum