let T be complete LATTICE; :: thesis: for N being net of
for M being subnet of N
for e being Embedding of M,N st ( for i being Element of
for j being Element of st e . j <= i holds
ex j' being Element of st
( j' >= j & N . i >= M . j' ) ) holds
lim_inf N = lim_inf M
let N be net of ; :: thesis: for M being subnet of N
for e being Embedding of M,N st ( for i being Element of
for j being Element of st e . j <= i holds
ex j' being Element of st
( j' >= j & N . i >= M . j' ) ) holds
lim_inf N = lim_inf M
let M be subnet of N; :: thesis: for e being Embedding of M,N st ( for i being Element of
for j being Element of st e . j <= i holds
ex j' being Element of st
( j' >= j & N . i >= M . j' ) ) holds
lim_inf N = lim_inf M
let e be Embedding of M,N; :: thesis: ( ( for i being Element of
for j being Element of st e . j <= i holds
ex j' being Element of st
( j' >= j & N . i >= M . j' ) ) implies lim_inf N = lim_inf M )
assume A1: for i being Element of
for j being Element of st e . j <= i holds
ex j' being Element of st
( j' >= j & N . i >= M . j' ) ; :: thesis: lim_inf N = lim_inf M
deffunc H₁( net of ) -> set = { ("/\" { ($1 . i) where i is Element of : i >= j } ,T) where j is Element of : verum } ;
"\/" H₁(N),T is_>=_than H₁(M)

proof

let t be Element of ; :: according to LATTICE3:def 9 :: thesis: ( not t in H₁(M) or t <= "\/" H₁(N),T )
assume t in H₁(M) ; :: thesis: t <= "\/" H₁(N),T
then consider j being Element of such that
A2: t = "/\" { (M . i) where i is Element of : i >= j } ,T ;
reconsider j = j as Element of ;
set j' = e . j;
set X = { (N . i) where i is Element of : i >= e . j } ;
set Y = { (M . i) where i is Element of : i >= j } ;
t is_<=_than { (N . i) where i is Element of : i >= e . j }

proof

let x be Element of ; :: according to LATTICE3:def 8 :: thesis: ( not x in { (N . i) where i is Element of : i >= e . j } or t <= x )
assume x in { (N . i) where i is Element of : i >= e . j } ; :: thesis: t <= x
then consider i being Element of such that
A3: x = N . i and
A4: i >= e . j ;
reconsider i = i as Element of ;
consider k being Element of such that
A5: k >= j and
A6: N . i >= M . k by A1, A4;
M . k in { (M . i) where i is Element of : i >= j } by A5;
then M . k >= t by A2, YELLOW_2:24;
hence t <= x by A3, A6, YELLOW_0:def 2; :: thesis: verum

end;

then A7: t <= "/\" { (N . i) where i is Element of : i >= e . j } ,T by YELLOW_0:33;
"/\" { (N . i) where i is Element of : i >= e . j } ,T in H₁(N) ;
then "/\" { (N . i) where i is Element of : i >= e . j } ,T <= "\/" H₁(N),T by YELLOW_2:24;
hence t <= "\/" H₁(N),T by A7, YELLOW_0:def 2; :: thesis: verum

end;

then "\/" H₁(N),T >= "\/" H₁(M),T by YELLOW_0:32;
then lim_inf N >= "\/" H₁(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; :: thesis: verum