let T be complete LATTICE; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( ( 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 ) ; :: thesis: lim_inf N = lim_inf M
deffunc H₁( net of T) -> set = { ("/\" ( { ($1 . i) where i is Element of $1 : i >= j } ,T)) where j is Element of $1 : verum } ;
"\/" (H₁(N),T) is_>=_than H₁(M)

proof

let t be Element of T; :: 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 M such that
A2: t = "/\" ( { (M . i) where i is Element of M : i >= j } ,T) ;
reconsider j = j as Element of M ;
set j9 = e . j;
set X = { (N . i) where i is Element of N : i >= e . j } ;
set Y = { (M . i) where i is Element of M : i >= j } ;
t is_<=_than { (N . i) where i is Element of N : i >= e . j }

proof

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

end;

then A7: t <= "/\" ( { (N . i) where i is Element of N : i >= e . j } ,T) by YELLOW_0:33;
"/\" ( { (N . i) where i is Element of N : i >= e . j } ,T) in H₁(N) ;
then "/\" ( { (N . i) where i is Element of N : i >= e . j } ,T) <= "\/" (H₁(N),T) by YELLOW_2:22;
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