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) ;
set e = the Embedding of M,N;
reconsider j = j as Element of N ;
consider j9 being Element of M such that
A3: for p being Element of M st j9 <= p holds
j <= the Embedding of M,N . 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 >= j9 } ;
A4: ex_inf_of { (N . i) where i is Element of N : i >= j } ,T by YELLOW_0:17;
A5: ex_inf_of { (M . i) where i is Element of M : i >= j9 } ,T by YELLOW_0:17;
{ (M . i) where i is Element of M : i >= j9 } c= { (N . i) where i is Element of N : i >= j }

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in { (M . i) where i is Element of M : i >= j9 } 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 >= j9 } ; :: thesis: y in { (N . i) where i is Element of N : i >= j }
then consider i being Element of M such that
A6: y = M . i and
A7: i >= j9 ;
reconsider i = i as Element of M ;
the Embedding of M,N . i >= j by A3, A7;
then N . ( the Embedding of M,N . 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 A6, Th36; :: thesis: verum

end;

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

end;

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