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 of 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 of 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 of 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 21;
then consider N, x being set such that
A3: ( N in NetUniv L1 & x in the carrier of L1 & [N1,a] = [N,x] ) by A2, ZFMISC_1:def 2;
reconsider x = x as Element of L1 by A3;
A4: ( N = N1 & x = a ) by A3, ZFMISC_1:33;
then consider N2 being strict net of L2 such that
A5: ( N2 in NetUniv 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, A3, Th3;
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 )
ex N being strict net of L1 st
( N = N1 & the carrier of N in the_universe_of the carrier of L1 ) by A3, A4, YELLOW_6:def 14;
then reconsider N1 = N1 as strict net of L1 ;

now

let M be subnet of N2; :: thesis: x = lim_inf M
consider M1 being strict subnet of N1 such that
A6: ( 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, A5, Th5;
thus x = lim_inf M1 by A2, A3, A4, WAYBEL28:def 3
.= lim_inf M by A1, A6, Th4 ; :: thesis: verum

end;

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, A4, A5, WAYBEL28:def 3; :: thesis: verum