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 net of L1

for N2 being net of L2 st 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 holds

lim_inf N1 = lim_inf 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 net of L1

for N2 being net of L2 st 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 holds

lim_inf N1 = lim_inf N2

let N1 be net of L1; :: thesis: for N2 being net of L2 st 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 holds

lim_inf N1 = lim_inf N2

let N2 be net of L2; :: thesis: ( 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 implies lim_inf N1 = lim_inf N2 )

assume A2: ( 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 ) ; :: thesis: lim_inf N1 = lim_inf N2

deffunc H_{1}( Element of N2) -> set = { (N2 . i) where i is Element of N2 : i >= $1 } ;

deffunc H_{2}( Element of N1) -> set = { (N1 . i) where i is Element of N1 : i >= $1 } ;

set U1 = { ("/\" (H_{2}(j),L1)) where j is Element of N1 : verum } ;

set U2 = { ("/\" (H_{1}(j),L2)) where j is Element of N2 : verum } ;

A3: ( lim_inf N1 = "\/" ( { ("/\" (H_{2}(j),L1)) where j is Element of N1 : verum } ,L1) & lim_inf N2 = "\/" ( { ("/\" (H_{1}(j),L2)) where j is Element of N2 : verum } ,L2) )
by WAYBEL11:def 6;

{ ("/\" (H_{2}(j),L1)) where j is Element of N1 : verum } c= the carrier of L1
_{2}(j),L1)) where j is Element of N1 : verum } as Subset of L1 ;

( not U1 is empty & U1 is directed ) by WAYBEL32:7;

then A4: ex_sup_of U1,L1 by WAYBEL_0:75;

( U1 c= { ("/\" (H_{1}(j),L2)) where j is Element of N2 : verum } & { ("/\" (H_{1}(j),L2)) where j is Element of N2 : verum } c= U1 )
by A1, A2, Lm2;

then U1 = { ("/\" (H_{1}(j),L2)) where j is Element of N2 : verum }
;

hence lim_inf N1 = lim_inf N2 by A1, A3, A4, YELLOW_0:26; :: thesis: verum

for N2 being net of L2 st 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 holds

lim_inf N1 = lim_inf 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 net of L1

for N2 being net of L2 st 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 holds

lim_inf N1 = lim_inf N2

let N1 be net of L1; :: thesis: for N2 being net of L2 st 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 holds

lim_inf N1 = lim_inf N2

let N2 be net of L2; :: thesis: ( 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 implies lim_inf N1 = lim_inf N2 )

assume A2: ( 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 ) ; :: thesis: lim_inf N1 = lim_inf N2

deffunc H

deffunc H

set U1 = { ("/\" (H

set U2 = { ("/\" (H

A3: ( lim_inf N1 = "\/" ( { ("/\" (H

{ ("/\" (H

proof

then reconsider U1 = { ("/\" (H
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { ("/\" (H_{2}(j),L1)) where j is Element of N1 : verum } or x in the carrier of L1 )

assume x in { ("/\" (H_{2}(j),L1)) where j is Element of N1 : verum }
; :: thesis: x in the carrier of L1

then ex j being Element of N1 st x = "/\" (H_{2}(j),L1)
;

hence x in the carrier of L1 ; :: thesis: verum

end;assume x in { ("/\" (H

then ex j being Element of N1 st x = "/\" (H

hence x in the carrier of L1 ; :: thesis: verum

( not U1 is empty & U1 is directed ) by WAYBEL32:7;

then A4: ex_sup_of U1,L1 by WAYBEL_0:75;

( U1 c= { ("/\" (H

then U1 = { ("/\" (H

hence lim_inf N1 = lim_inf N2 by A1, A3, A4, YELLOW_0:26; :: thesis: verum