let L be complete LATTICE; :: thesis: for N being net of L holds inf N <= lim_inf N
let N be net of L; :: thesis: inf N <= lim_inf N
set X = { ("/\" ( { (N . i) where i is Element of N : i >= j1 } ,L)) where j1 is Element of N : verum } ;
{ ("/\" ( { (N . i) where i is Element of N : i >= j1 } ,L)) where j1 is Element of N : verum } c= the carrier of L

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { ("/\" ( { (N . i) where i is Element of N : i >= j1 } ,L)) where j1 is Element of N : verum } or x in the carrier of L )
assume x in { ("/\" ( { (N . i) where i is Element of N : i >= j1 } ,L)) where j1 is Element of N : verum } ; :: thesis: x in the carrier of L
then ex j1 being Element of N st x = "/\" ( { (N . i) where i is Element of N : i >= j1 } ,L) ;
hence x in the carrier of L ; :: thesis: verum

end;

then reconsider X = { ("/\" ( { (N . i) where i is Element of N : i >= j1 } ,L)) where j1 is Element of N : verum } as Subset of L ;
set j = the Element of N;
A1: { (N . i) where i is Element of N : i >= the Element of N } c= rng the mapping of N

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (N . i) where i is Element of N : i >= the Element of N } or x in rng the mapping of N )
A2: dom the mapping of N = the carrier of N by FUNCT_2:def 1;
assume x in { (N . i) where i is Element of N : i >= the Element of N } ; :: thesis: x in rng the mapping of N
then consider i being Element of N such that
A3: x = N . i and
i >= the Element of N ;
x = the mapping of N . i by A3, WAYBEL_0:def 8;
hence x in rng the mapping of N by A2, FUNCT_1:def 3; :: thesis: verum

end;

reconsider X = X as Subset of L ;
set x = "/\" ( { (N . i) where i is Element of N : i >= the Element of N } ,L);
( ex_inf_of { (N . i) where i is Element of N : i >= the Element of N } ,L & ex_inf_of rng the mapping of N,L ) by YELLOW_0:17;
then "/\" ( { (N . i) where i is Element of N : i >= the Element of N } ,L) >= "/\" ((rng the mapping of N),L) by A1, YELLOW_0:35;
then "/\" ( { (N . i) where i is Element of N : i >= the Element of N } ,L) >= Inf by YELLOW_2:def 6;
then A4: inf N <= "/\" ( { (N . i) where i is Element of N : i >= the Element of N } ,L) by WAYBEL_9:def 2;
ex_sup_of X,L by YELLOW_0:17;
then ( "/\" ( { (N . i) where i is Element of N : i >= the Element of N } ,L) in X & X is_<=_than "\/" (X,L) ) by YELLOW_0:def 9;
then "/\" ( { (N . i) where i is Element of N : i >= the Element of N } ,L) <= "\/" (X,L) by LATTICE3:def 9;
hence inf N <= lim_inf N by A4, YELLOW_0:def 2; :: thesis: verum