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 ;

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

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

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 )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;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

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