let T be complete LATTICE; for N being net of T
for M being subnet of N
for e being Embedding of M,N st ( for i being Element of N
for j being Element of M st e . j <= i holds
ex j9 being Element of M st
( j9 >= j & N . i >= M . j9 ) ) holds
lim_inf N = lim_inf M
let N be net of T; for M being subnet of N
for e being Embedding of M,N st ( for i being Element of N
for j being Element of M st e . j <= i holds
ex j9 being Element of M st
( j9 >= j & N . i >= M . j9 ) ) holds
lim_inf N = lim_inf M
let M be subnet of N; for e being Embedding of M,N st ( for i being Element of N
for j being Element of M st e . j <= i holds
ex j9 being Element of M st
( j9 >= j & N . i >= M . j9 ) ) holds
lim_inf N = lim_inf M
let e be Embedding of M,N; ( ( for i being Element of N
for j being Element of M st e . j <= i holds
ex j9 being Element of M st
( j9 >= j & N . i >= M . j9 ) ) implies lim_inf N = lim_inf M )
assume A1:
for i being Element of N
for j being Element of M st e . j <= i holds
ex j9 being Element of M st
( j9 >= j & N . i >= M . j9 )
; lim_inf N = lim_inf M
deffunc H1( net of T) -> set = { ("/\" ( { ($1 . i) where i is Element of $1 : i >= j } ,T)) where j is Element of $1 : verum } ;
"\/" (H1(N),T) is_>=_than H1(M)
then
"\/" (H1(N),T) >= "\/" (H1(M),T)
by YELLOW_0:32;
then
lim_inf N >= "\/" (H1(M),T)
by WAYBEL11:def 6;
then A8:
lim_inf N >= lim_inf M
by WAYBEL11:def 6;
lim_inf M >= lim_inf N
by Th37;
hence
lim_inf N = lim_inf M
by A8, YELLOW_0:def 3; verum