theorem Th6: :: WAYBEL33:6

for L1, L2 being up-complete /\-complete Semilattice st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) holds
for N1 being NetStr over L1
for a being set st [N1,a] in lim_inf-Convergence L1 holds
ex N2 being strict net of L2 st
( [N2,a] in lim_inf-Convergence L2 & RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of N2, the InternalRel of N2 #) & the mapping of N1 = the mapping of N2 )