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 j' being Element of M st
( j' >= j & N . i >= M . j' ) ) 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 j' being Element of M 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 N
for j being Element of M st e . j <= i holds
ex j' being Element of M 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 N
for j being Element of M st e . j <= i holds
ex j' being Element of M st
( j' >= j & N . i >= M . j' ) ) 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 j' being Element of M st
( j' >= j & N . i >= M . j' ) ; :: 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 j' = 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 & i >= e . j ) ;
reconsider i = i as Element of N ;
consider k being Element of M such that
A4: ( k >= j & N . i >= M . k ) by A1, A3;
M . k in { (M . i) where i is Element of M : i >= j } by A4;
then M . k >= t by A2, YELLOW_2:24;
hence t <= x by A3, A4, YELLOW_0:def 2; :: thesis: verum

end;

then A5: 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:24;
hence t <= "\/" H₁(N),T by A5, 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 ( lim_inf N >= lim_inf M & lim_inf M >= lim_inf N ) by Th37, WAYBEL11:def 6;
hence lim_inf N = lim_inf M by YELLOW_0:def 3; :: thesis: verum