let L1, L2 be up-complete /\-complete Semilattice; ( 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 #)
; 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; 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 ; ( [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
; 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 for M being subnet of N2 holds x = lim_inf Mlet M be
subnet of
N2;
x = lim_inf Mconsider 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
;
verum end;
take
N2
; ( [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; verum