let L1, L2 be up-complete /\-complete Semilattice; :: thesis: ( RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) implies 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 ) )
assume A1: RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) ; :: thesis: 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 )
let N1 be NetStr over L1; :: thesis: 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 )
let a be set ; :: thesis: ( [N1,a] in lim_inf-Convergence L1 implies 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 ) )
assume A2: [N1,a] in lim_inf-Convergence L1 ; :: thesis: 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 )
lim_inf-Convergence L1 c= [:(NetUniv L1), the carrier of L1:] by YELLOW_6:def 18;
then consider N, x being object such that
A3: N in NetUniv L1 and
A4: x in the carrier of L1 and
A5: [N1,a] = [N,x] by A2, ZFMISC_1:def 2;
reconsider x = x as Element of L1 by A4;
A6: N = N1 by A5, XTUPLE_0:1;
then consider N2 being strict net of L2 such that
A7: N2 in NetUniv L2 and
A8: ( 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 ) by A1, A3, Th3;
ex N being strict net of L1 st
( N = N1 & the carrier of N in the_universe_of the carrier of L1 ) by A3, A6, YELLOW_6:def 11;
then reconsider N1 = N1 as strict net of L1 ;

A9: now :: thesis: for M being subnet of N2 holds x = lim_inf M

let M be subnet of N2; :: thesis: x = lim_inf M
consider M1 being strict subnet of N1 such that
A10: ( RelStr(# the carrier of M, the InternalRel of M #) = RelStr(# the carrier of M1, the InternalRel of M1 #) & the mapping of M = the mapping of M1 ) by A1, A8, Th5;
thus x = lim_inf M1 by A2, A3, A5, A6, WAYBEL28:def 3
.= lim_inf M by A1, A10, Th4 ; :: thesis: verum

end;

take N2 ; :: thesis: ( [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 )
x = a by A5, XTUPLE_0:1;
hence ( [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 ) by A1, A7, A8, A9, WAYBEL28:def 3; :: thesis: verum