let T be complete LATTICE; :: thesis: for N being net of T
for M being subnet of N holds lim_inf N <= lim_inf M
let N be net of T; :: thesis: for M being subnet of N holds lim_inf N <= lim_inf M
let M be subnet of N; :: 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 } ;
A1: "\/" H₁(M),T is_>=_than H₁(N)

proof

let t be Element of T; :: according to LATTICE3:def 9 :: thesis: ( not t in H₁(N) or t <= "\/" H₁(M),T )
assume t in H₁(N) ; :: thesis: t <= "\/" H₁(M),T
then consider j being Element of N such that
A2: t = "/\" { (N . i) where i is Element of N : i >= j } ,T ;
consider e being Embedding of M,N;
reconsider j = j as Element of N ;
consider j' being Element of M such that
A3: for p being Element of M st j' <= p holds
j <= e . p by Def3;
set X = { (N . i) where i is Element of N : i >= j } ;
set Y = { (M . i) where i is Element of M : i >= j' } ;
A4: ( ex_inf_of { (N . i) where i is Element of N : i >= j } ,T & ex_inf_of { (M . i) where i is Element of M : i >= j' } ,T ) by YELLOW_0:17;
{ (M . i) where i is Element of M : i >= j' } c= { (N . i) where i is Element of N : i >= j }

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in { (M . i) where i is Element of M : i >= j' } or y in { (N . i) where i is Element of N : i >= j } )
assume y in { (M . i) where i is Element of M : i >= j' } ; :: thesis: y in { (N . i) where i is Element of N : i >= j }
then consider i being Element of M such that
A5: ( y = M . i & i >= j' ) ;
reconsider i = i as Element of M ;
e . i >= j by A3, A5;
then N . (e . i) in { (N . i) where i is Element of N : i >= j } ;
hence y in { (N . i) where i is Element of N : i >= j } by A5, Th36; :: thesis: verum

end;

then A6: t <= "/\" { (M . i) where i is Element of M : i >= j' } ,T by A2, A4, YELLOW_0:35;
"/\" { (M . i) where i is Element of M : i >= j' } ,T in H₁(M) ;
then "/\" { (M . i) where i is Element of M : i >= j' } ,T <= "\/" H₁(M),T by YELLOW_2:24;
hence t <= "\/" H₁(M),T by A6, YELLOW_0:def 2; :: thesis: verum

end;

( lim_inf M = "\/" H₁(M),T & lim_inf N = "\/" H₁(N),T ) by WAYBEL11:def 6;
hence lim_inf N <= lim_inf M by A1, YELLOW_0:32; :: thesis: verum